Function lambda_calculus::data::num::church::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::data::num::church::pred;
use lambda_calculus::*;

assert_eq!(beta(app(pred(), 1.into_church()), NOR, 0), 0.into_church());
assert_eq!(beta(app(pred(), 3.into_church()), NOR, 0), 2.into_church());