curry-howard

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

Diffstat

2 files changed, 4 insertions, 4 deletions

diff --git a/examples/eq.lean b/examples/eq.lean
@@ -1,4 +1,4 @@
-inductive eq (x : t) (y : t) : Prop
+inductive eq (x y : t) : Prop
 | rfl : eq x x
 
 infix = := eq

diff --git a/examples/types.lean b/examples/types.lean
@@ -1,7 +1,7 @@
--- a e b <-> And a b
-inductive and (a : Prop) (b : Prop) : Prop
+-- a e b <-> and a b
+inductive and (a b : Prop) : Prop
 | intro : a → b → and a b
 
-inductive or (a : Prop) (b : Prop) : Prop
+inductive or (a b : Prop) : Prop
 | inl : a → or a b
 | inr : b → or a b