Function lambda_calculus::arithmetic::eq

pub fn eq() -> Term

Applied to two Church-encoded numbers it returns a Church-encoded boolean indicating whether its first argument is egual to the second one.

EQ := λmn.AND (LEQ m n) (LEQ n m) = λ λ AND (LEQ 2 1) (LEQ 1 2)

Example

use lambda_calculus::arithmetic::{zero, one, eq};
use lambda_calculus::booleans::{tru, fls};
use lambda_calculus::reduction::normalize;

assert_eq!(normalize(eq().app(zero()).app(zero())), tru());
assert_eq!(normalize(eq().app(one()).app(one())),   tru());
assert_eq!(normalize(eq().app(zero()).app(one())),  fls());
assert_eq!(normalize(eq().app(one()).app(zero())),  fls());