- Commit
- 7d55c1ed4b9378815f9d72eaecee4087b37d09cc
- Parent
- 5bf1a87a617e426b842f3b7c5f6aaa0317dd192f
- Author
- Pablo <pablo-escobar@riseup.net>
- Date
Updated an example
Slides of a (very) informal lecture of mine on the Curry-Howard correspondence
Updated an example
2 files changed, 1 insertion, 1 deletion
Status | File Name | N° Changes | Insertions | Deletions |
Modified | examples/example.lean | 2 | 1 | 1 |
Modified | main.pdf | 0 | 0 | 0 |
diff --git a/examples/example.lean b/examples/example.lean @@ -1,4 +1,4 @@ -theorem ex : Or p q → Or q p := by +theorem ex : Or p q -> Or q p := by intro h match h with | Or.inl _ =>