curry-howard

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

File Name	Size	Mode
types.lean	161B	-rw-r--r--

1 -- p e q <-> and p q
2 inductive and (p q : Prop) : Prop
3 | intro : p → q → and p q
4 
5 inductive or (p q : Prop) : Prop
6 | inl : p → or p q
7 | inr : q → or p q