curry-howard

Slides of a (very) informal lecture of mine on the Curry-Howard correspondence

File Name Size Mode
nat.lean 55B -rw-r--r--
1 inductive ℕ : Type
2 | zero : ℕ
3 | succ : ℕ → ℕ