Proposal: Data.Bool.implies

Petr Pudlák petr.mvd at gmail.com
Tue Jan 19 18:38:37 UTC 2016


+1 for distinguishing <= and implies. Ordering should not be tied to
logical meaning.

po 18. 1. 2016 v 19:38 odesílatel Henning Thielemann <
lemming at henning-thielemann.de> napsal:

>
> On Mon, 18 Jan 2016, Brent Yorgey wrote:
>
> > I disagree.  The equivalence between `implies` and (<=) depends on the
> > ordering chosen for Bool, which is completely arbitrary, and is not
> > something people thinking about logic should be expected to know or
> > learn.  For example, the Coq standard library happens to choose the
> > other order, with True < False.
>
> I can confirm that the order is arbitrary. I used a Modula II
> implementation where True was represented as -1, because that is the bit
> pattern where all bits are
> set._______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20160119/e7e1c42a/attachment.html>


More information about the Libraries mailing list