Closed
Description
So: (DRAFT)
- issue Possible Regression at fromℕ< #1988
- the discussion around Should the constructors of
Data.Nat._≤_
be declared asinstance
s? #1951 - ditto. regarding An alternative to #1698 #1709 and friends
- @MatthewDaggitt 's heroic work on Switch
Positive/Negative/etc.
to use irrelevant instance arguments #1581 RFC: changed_/_
and_%_
to use irrelevant instance arguments #1538 etc. - etc.
lead me to conclude that we should add (!?) an irrelevant-instance version of LessThan
to Data.Nat.Base
, along the analogy with NonZero
, and forever after use this relation for 'computational' appeals to _<_
, such as in the (old/refactored; mea culpa) definition of fromN<
...
... the only question being whether this can already be achieved by back-porting Positive
etc. to Data.Nat
, as any instance of LessThan m n
(sic) defined in terms of _<ᵇ_
would eventually reduce to one of Positive k
for some k
? or else defining Positive
in terms of LessThan
?