Function lambda_calculus::arithmetic::pred

pub fn pred() -> Term

Applied to a Church-encoded number it produces its predecessor.

PRED := λnfx.n (λgh.h (g f)) (λu.x) (λu.u) = λ λ λ 3 (λ λ 1 (2 4)) (λ 2) (λ 1)

Example

use lambda_calculus::arithmetic::pred;

let mut expr = pred().app(3.into());
expr.beta_full();

assert_eq!(expr, 2.into());