Function lambda_calculus::arithmetic::gt

pub fn gt() -> Term

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

GT := λab.NOT (LEQ a b) = λ λ NOT (LEQ 2 1)

Examples

use lambda_calculus::arithmetic::{zero, one, gt};
use lambda_calculus::booleans::{tru, fls};
use lambda_calculus::reduction::beta_full;

assert_eq!(beta_full(gt().app(0.into()).app(0.into())), fls());
assert_eq!(beta_full(gt().app(1.into()).app(1.into())), fls());
assert_eq!(beta_full(gt().app(0.into()).app(1.into())), fls());
assert_eq!(beta_full(gt().app(1.into()).app(0.into())), tru());