Function lambda_calculus::data::num::scott::succ

source ·

pub fn succ() -> Term

Expand description

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

SUCC ≡ λnxy.y n ≡ λ λ λ 1 3

Example

use lambda_calculus::data::num::scott::succ;
use lambda_calculus::*;

assert_eq!(beta(app(succ(), 0.into_scott()), NOR, 0), 1.into_scott());
assert_eq!(beta(app(succ(), 1.into_scott()), NOR, 0), 2.into_scott());