74 lines
1.8 KiB
Plaintext
74 lines
1.8 KiB
Plaintext
module Lennart where
|
|
|
|
-- stack exec -- pi-forall Lennart.pi
|
|
-- with unbind / subst
|
|
-- 7.81s user 0.52s system 97% cpu 8.568 total
|
|
-- with substBind
|
|
-- 3.81s user 0.28s system 94% cpu 4.321 total
|
|
import Fix
|
|
|
|
bool : Type
|
|
bool = [C : Type] -> C -> C -> C
|
|
|
|
false : bool
|
|
false = \[C]. \f.\t.f
|
|
true : bool
|
|
true = \[C]. \f.\t.t
|
|
|
|
nat : Type
|
|
nat = [C : Type] -> C -> (nat -> C) -> C
|
|
zero : nat
|
|
zero = \[C].\z.\s.z
|
|
succ : nat -> nat
|
|
succ = \n.\[C].\z.\s. s n
|
|
one : nat
|
|
one = succ zero
|
|
two : nat
|
|
two = succ one
|
|
three : nat
|
|
three = succ two
|
|
isZero : nat -> bool
|
|
isZero = \n.n [bool] true (\m.false)
|
|
const : [A:Type] -> A -> A -> A
|
|
const = \[A].\x.\y.x
|
|
prod : Type -> Type -> Type
|
|
prod = \A B. [C:Type] -> (A -> B -> C) -> C
|
|
pair : [A :Type] -> [B: Type] -> A -> B -> prod A B
|
|
pair = \[A][B] a b. \[C] p. p a b
|
|
fst : [A:Type] -> [B:Type] -> prod A B -> A
|
|
fst = \[A][B] ab. ab [A] (\a.\b.a)
|
|
snd : [A:Type] -> [B:Type] -> prod A B -> B
|
|
snd = \[A][B] ab.ab [B] (\a.\b.b)
|
|
add : nat -> nat -> nat
|
|
add = fix [nat -> nat -> nat]
|
|
\radd . \x.\y. x [nat] y (\ n. succ (radd n y))
|
|
mul : nat -> nat -> nat
|
|
mul = fix [nat -> nat -> nat]
|
|
\rmul. \x.\y. x [nat] zero (\ n. add y (rmul n y))
|
|
fac : nat -> nat
|
|
fac = fix [nat -> nat]
|
|
\rfac. \x. x [nat] one (\ n. mul x (rfac n))
|
|
eqnat : nat -> nat -> bool
|
|
eqnat = fix [nat -> nat -> bool]
|
|
\reqnat. \x. \y.
|
|
x [bool]
|
|
(y [bool] true (\b.false))
|
|
(\x1.y [bool] false (\y1. reqnat x1 y1))
|
|
sumto : nat -> nat
|
|
sumto = fix [nat -> nat]
|
|
\rsumto. \x. x [nat] zero (\n. add x (rsumto n))
|
|
n5 : nat
|
|
n5 = add two three
|
|
n6 : nat
|
|
n6 = add three three
|
|
n17 : nat
|
|
n17 = add n6 (add n6 n5)
|
|
n37 : nat
|
|
n37 = succ (mul n6 n6)
|
|
n703 : nat
|
|
n703 = sumto n37
|
|
n720 : nat
|
|
n720 = fac n6
|
|
|
|
t : (eqnat n720 (add n703 n17)) = true
|
|
t = Refl |