Function lambda_calculus::data::num::parigot::sub

pub fn sub() -> Term

Applied to two Church-encoded numbers it subtracts the second one from the first one.

SUB ≡ λnm.m (λp. PRED) n ≡ λ λ 1 (λ PRED) 2

Example

use lambda_calculus::data::num::parigot::sub;
use lambda_calculus::*;

assert_eq!(beta(app!(sub(), 1.into_parigot(), 0.into_parigot()), NOR, 0), 1.into_parigot());
assert_eq!(beta(app!(sub(), 3.into_parigot(), 1.into_parigot()), NOR, 0), 2.into_parigot());
assert_eq!(beta(app!(sub(), 5.into_parigot(), 2.into_parigot()), NOR, 0), 3.into_parigot());