lemming at henning-thielemann.de
Mon Jan 18 18:38:01 UTC 2016
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.
More information about the Libraries