プログラミング言語 Proxima

id ::= \x -> x

pred ::= succ \x -> x

Nat ::= zero | succ Nat

nat \z \s
    ::= zero -> z
    | succ \n -> s (nat z s n)

Nat + Nat :: Nat
\x + \y = nat x succ y

Nat - Nat :: Nat
\x - \y = nat x (pred | id) y