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());