Function lambda_calculus::arithmetic::neq
[−]
[src]
pub fn neq() -> Term
Applied to two Church-encoded numbers it returns a Church-encoded boolean indicating whether its first argument is not egual to the second one.
NEQ := λab.OR (NOT (LEQ a b)) (NOT (LEQ b a)) = λ λ OR (NOT (LEQ 2 1)) (NOT (LEQ 1 2))
Examples
use lambda_calculus::arithmetic::neq; use lambda_calculus::booleans::{tru, fls}; use lambda_calculus::reduction::beta_full; assert_eq!(beta_full(neq().app(0.into()).app(0.into())), fls()); assert_eq!(beta_full(neq().app(1.into()).app(1.into())), fls()); assert_eq!(beta_full(neq().app(0.into()).app(1.into())), tru()); assert_eq!(beta_full(neq().app(1.into()).app(0.into())), tru());