Function lambda_calculus::arithmetic::succ

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::succ;

let mut expr = succ().app(0.into());
expr.beta_full();

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