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::{zero, one, plus};
use lambda_calculus::reduction::normalize;

assert_eq!(normalize(plus().app(zero()).app(one())), one());