pub fn sub() -> Term
Expand description
Applied to two Church-encoded numbers it subtracts the second one from the first one.
SUB ≡ λab.b PRED a ≡ λ λ 1 PRED 2
Example
use lambda_calculus::data::num::church::sub;
use lambda_calculus::*;
assert_eq!(beta(app!(sub(), 1.into_church(), 0.into_church()), NOR, 0), 1.into_church());
assert_eq!(beta(app!(sub(), 3.into_church(), 1.into_church()), NOR, 0), 2.into_church());
assert_eq!(beta(app!(sub(), 5.into_church(), 2.into_church()), NOR, 0), 3.into_church());