curry-howard

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

File Name	Size	Mode
example.lean	122B	-rw-r--r--

1 lemma ex : or p q → or q p := by
2   intro h
3   match h with
4   | inl h1 =>
5     exact inr h1
6   | inr h2 =>
7     exact inl h2