search

bor0 / gidti

Book: Introduction to Dependent Types with Idris
https://leanpub.com/gidti
Other
76 stars 4 forks source link

Alter examples for the implication connective #18

Closed nbloomf closed 6 years ago

nbloomf commented 6 years ago

I changed the examples under "implication" here. When I taught logic students found the promise interpretation to be helpful for understanding why vacuous implications default to true.

(Let me know if these edits are too much!)

bor0 commented 6 years ago

Let me know if these edits are too much!

These are more than welcome, as long as they make the introduction gentler :)