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

[Jon Fairbairn]

R J <rj248842 at hotmail.com> 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 at cl.cam.ac.uk