Slides of a (very) informal lecture of mine on the Curry-Howard correspondence
types.lean (161B)
1 -- p e q <-> and p q
2 inductive and (p q : Prop) : Prop
3 | intro : p → q → and p q
45 inductive or (p q : Prop) : Prop
6 | inl : p → or p q
7 | inr : q → or p q