Function lambda_calculus::data::num::parigot::succ

source ·

pub fn succ() -> Term

Expand description

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

SUCC ≡ λnsz.s n (n s z) ≡ λ λ λ 2 3 (3 2 1)

Example

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

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