Input

Output

Untyped Lambda Calculus Prelude

id = \x. x

-- Booleans
true = \x. \y. x
false = \x. \y. y

-- Pairs
MkPair = \a. \b. \x. x a b
fst = \p. p true
snd = \p. p false

-- Natural numbers
zero = \f. \x. x
succ = \n. \f. \x. f (n f x)

-- (for convenience, you can use integer literals)
three = 3

-- predecessor of a natural number (pred 4 == 3)
pred = \n. fst (predHelper n)
predHelper = \n. n (\p. \x. x (snd p) (succ (snd p))) (MkPair 0 0)

isZero = \n. n (\t. false) true

plus = \n. \m. \f. \x. n f (m f x)
minus = \n. \m. m pred n
mult = \n. \m. n (plus m) 0
exp = \n. \m. m (mult n) 1
    

Simply Typed Lambda Calculus Prelude

-- Natural numbers
succ = \n : (N -> N) -> N -> N. \f : N -> N. \x : N. f (n f x)
plus = \n : (N -> N) -> N -> N. \m : (N -> N) -> N -> N. \f : N -> N. \x : N. n f (m f x)
mult = \n : (N -> N) -> N -> N. \m : (N -> N) -> N -> N. \f : N -> N. \x : N. n (m f) x
    

System T Prelude

-- Natural numbers:
-- Succ and Zero are built in
-- As is Rec, the generic recursion combinator

plus = \m : Nat. \n : Nat. Rec (\x : Nat. \k : Nat. Succ k) m n
mult = \m : Nat. \n : Nat. Rec (\x : Nat. \k : Nat. plus k m) 0 n
    

λP Prelude

plus : forall (n : Nat). forall (m : Nat). Nat
plus = (\n. \m. natElim (\_. Nat) n (\k. \rec. S rec) m)

mult : forall (n : Nat). forall (m : Nat). Nat
mult = (\n. \m. natElim (\_. Nat) Z (\k. \recn. plus recn n) m)

dec : forall (n : Nat). Nat
dec = \n. natElim (\_. Nat) Z (\k. \rec. k) n

sub : forall (n : Nat). forall (m : Nat). Nat
sub = \n. \m. natElim (\_. Nat) n (\k. \rec. dec rec) m

isZero : forall (n : Nat). Bool
isZero = \n. natElim (\_. Bool) True (\_. \_. False) n

natEq : forall (n : Nat). forall (m : Nat). Bool
natEq = \m. \n. natElim (\_. forall (_ : Nat). Bool) (\k. natElim  (\_. Bool) True (\_. \_. False) k) (\j. \rec. \n. natElim (\_. Bool) False (\k. \_. rec k) n) m n

-- N.B. this doesn't quite work yet
append : forall (a : Type). forall (k1 : Nat). forall (v1 : Vec a k1). forall (k2 : Nat). forall (v2: Vec a k2). Vec a (plus k1 k2) 
append = (\a. \k1. \v1. \k2. \v2. vecElim a (\m. \_. Vec a (plus k1 m)) v1 (\m. \v. \vs. \rec. VCons a (S m) v rec) k2 v2)