Function lambda_calculus::arithmetic::succ [] [src]

pub fn succ() -> Term

Applied to a Church-encoded number it produces its successor.

SUCC := λnfx.f (n f x) = λ λ λ 2 (3 2 1)

Example

use lambda_calculus::arithmetic::{zero, one, succ};
use lambda_calculus::reduction::normalize;

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