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

[Jon Fairbairn]

Alexander Solla <ajs at 2piix.com> writes:

> On May 23, 2010, at 1:35 AM, Jon Fairbairn wrote:
>
>> 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.
>
> I don't see how that can be (but if you have a counter
> example, please show us). 

Oops! I was thinking of the symmetry rule in general. What I
said applies to “a && b” and not to “a == b”, but my point was
that surely you can’t be sure of that until after you’ve
finished a proof that does consider ⊥?

-- 
Jón Fairbairn                                 Jon.Fairbairn at cl.cam.ac.uk
http://www.chaos.org.uk/~jf/Stuff-I-dont-want.html  (updated 2009-01-31)