Alexander Solla
On May 22, 2010, at 1:32 AM, Jon Fairbairn wrote:
Since Bool is a type, and all Haskell types include ⊥, you need to add conditions in your proofs to exclude it.
Not really. Bottom isn't a value, so much as an expression for computations that don't refer to "real" values. It's close enough to be treated as a value in many contexts, but this isn't one of them.
It seems to me relevant here, because one of the uses to which one might put the symmetry rule is to replace an expression “e1 == e2” with “e2 == e1”, which can turn a programme that terminates into a programme that does not. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html (updated 2009-01-31)