curry-howard

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

File Name	Size	Mode
eq.lean	60B	-rw-r--r--

1 inductive eq (x y : t) : Prop
2 | rfl : eq x x
3 
4 infix = := eq