The laws for Eq are defined by asserting that the == decision procedure actually Reflects the type of propositional equality ≡, while the laws for Ord do not use this reflection style and just enumerate all the expected properties in a style suffering from "boolean blindness".
We should be consistent on how we go about all these similar situations, and in particular think how we should inter-operate with the standard library. (e.g. given that Ord reflects a definition that is not built-in like equality, but could be imported from stdlib's Data.Nat (≤), etc.).
The laws for
Eqare defined by asserting that the==decision procedure actuallyReflects the type of propositional equality≡, while the laws forOrddo not use this reflection style and just enumerate all the expected properties in a style suffering from "boolean blindness".We should be consistent on how we go about all these similar situations, and in particular think how we should inter-operate with the standard library. (e.g. given that
Ordreflects a definition that is not built-in like equality, but could be imported from stdlib'sData.Nat (≤), etc.).