Function lambda_calculus::data::num::church::leq

source ·
pub fn leq() -> Term
Expand description

Applied to two Church-encoded numbers it returns a lambda-encoded boolean indicating whether its first argument is less than or equal to the second one.

LEQ ≡ λmn.IS_ZERO (SUB m n) ≡ λ λ IS_ZERO (SUB 2 1)

Examples

use lambda_calculus::data::num::church::leq;
use lambda_calculus::*;

assert_eq!(beta(app!(leq(), 0.into_church(), 0.into_church()), NOR, 0), true.into());
assert_eq!(beta(app!(leq(), 1.into_church(), 1.into_church()), NOR, 0), true.into());
assert_eq!(beta(app!(leq(), 0.into_church(), 1.into_church()), NOR, 0), true.into());
assert_eq!(beta(app!(leq(), 1.into_church(), 0.into_church()), NOR, 0), false.into());