[Haskell-cafe] Re: Proof question -- (==) over Bool

R J writes:

I'm trying to prove that (==) is reflexive, symmetric, and transitive over the Bools, given this definition:

(==):: Bool -> Bool -> Bool x == y = (x && y) || (not x && not y)

Since Bool is a type, and all Haskell types include ⊥, you need to add conditions in your proofs to exclude it. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk