Alexander Solla <a...@2piix.com> writes: > 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.fairba...@cl.cam.ac.uk http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html (updated 2009-01-31) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe