Function lambda_calculus::arithmetic::plus [] [src]

pub fn plus() -> Term

Applied to two Church-encoded numbers it produces their sum.

PLUS := λmnfx.m f (n f x) = λ λ λ λ 4 2 (3 2 1)

Example

use lambda_calculus::arithmetic::plus;

let mut expr = plus().app(3.into()).app(2.into());
expr.beta_full();

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