Function lambda_calculus::arithmetic::sub

pub fn sub() -> Term

Applied to two Church-encoded numbers it subtracts the second one from the first one.

SUB := λmn.n PRED m = λ λ 1 PRED 2

Example

use lambda_calculus::arithmetic::sub;

let mut expr = sub().app(5.into()).app(3.into());
expr.beta_full();

assert_eq!(expr, 2.into());