Function lambda_calculus::arithmetic::leq
[−]
[src]
pub fn leq() -> Term
Applied to two Church-encoded numbers it returns a Church-encoded boolean indicating whether its first argument is less than or egual to the second one.
LEQ := λmn.IS_ZERO (SUB m n) = λ λ IS_ZERO (SUB 2 1)
Examples
use lambda_calculus::arithmetic::leq; use lambda_calculus::booleans::{tru, fls}; use lambda_calculus::reduction::beta_full; assert_eq!(beta_full(leq().app(0.into()).app(0.into())), tru()); assert_eq!(beta_full(leq().app(1.into()).app(1.into())), tru()); assert_eq!(beta_full(leq().app(0.into()).app(1.into())), tru()); assert_eq!(beta_full(leq().app(1.into()).app(0.into())), fls());