Function lambda_calculus::data::num::scott::pred

source ·

pub fn pred() -> Term

Expand description

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

PRED ≡ λn.n ZERO (λx.x) ≡ λ 1 ZERO (λ 1)

Example

use lambda_calculus::data::num::scott::pred;
use lambda_calculus::*;

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