Looks good to me! Do you have an opinion about infixl vs infixr?

On Mon, Sep 17, 2018, 5:21 AM Dannyu NDos <ndospark320@gmail.com> wrote:


---------- Forwarded message ---------
From: Dannyu NDos <ndospark320@gmail.com>
Date: 2018년 9월 17일 (월) 오후 6:18
Subject: Re: Add fixity for (==) and (/=)
To: <david.feuer@gmail.com>


Proof by truth table (F is False, T is True):
p q r (p == q) (q == r) ((p == q) == r) (p == (q == r))
F F F        T        T               F               F
F F T        T        F               T               T
F T F        F        F               T               T
F T T        F        T               F               F
T F F        F        T               T               T
T F T        F        F               F               F
T T F        T        F               F               F
T T T        T        T               T               T
That proves associativity of (==).

Also note that p /= q ≡ not p == q. Proof:
p q (p /= q) (not p) (not p == q)
F F        F       T            F
F T        T       T            T
T F        T       F            T
T T        F       F            F
And by symmetry of (/=), p /= q ≡ p == not q.

Then:
(p /= q) /= r ≡ (not p == q) == not r ≡ not p == (q == not r) ≡ p /= (q /= r).
Hence (/=) is associative.

Q.E.D.
_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries