search

bor0 / gidti

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

3.1 logical connectives commutativity #5

Closed Chobbes closed 6 years ago

Chobbes commented 6 years ago

Why do we mention that the connectives are commutative? That seems like something you could prove later instead? Also introducing commutativity with oplus (a different operator) would be confusing to beginners, since it's not clear that this means /\ or \/. If you have to have this comment, then I'd probably just include both a /\ b = b /\ a and a \/ b = b \/ a to keep things simple for the reader.

Chobbes commented 6 years ago

To clarify, I don't think that this comment adds anything at this stage in the book?

bor0 commented 6 years ago

We do prove them later. I agree it's a distraction at this point 👍

bor0 commented 6 years ago

Fixed in 729b4e20d6909b2ff9569fd5701338a76775c905.