Skip to content

Instantly share code, notes, and snippets.

@haitlahcen

haitlahcen/nat.k

Created January 3, 2019 08:24
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save haitlahcen/8fbd45d0ffc6a2c316204cd4cf981511 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save haitlahcen/8fbd45d0ffc6a2c316204cd4cf981511 to your computer and use it in GitHub Desktop.
Download ZIP
Boehm berrarduci nat
Raw
nat.k
(Lam Nat:*.
Lam s:Nat -> Nat.
Lam z:Nat.
Lam fold:Nat -> Pi R:*. (R -> R) -> R -> R.
Lam A:*.
Lam x:A.
fold (s (s (s (s z)))) A (Lam x:A. x) x)
(Pi Nat:*. (Nat -> Nat) -> Nat -> Nat)
(Lam Number:Pi N:*. (N -> N) -> N -> N.
Lam Nat:*.
Lam s: Nat -> Nat.
Lam z: Nat.
s (Number Nat s z))
(Lam Nat:*.
Lam s: Nat -> Nat.
Lam z: Nat.
z)
(Lam Number:Pi N:*. (N -> N) -> N -> N. Number)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment