[Agda] _<=_ and _<_
mechvel at botik.ru
Tue Sep 24 20:33:48 CEST 2013
On Tue, 2013-09-24 at 17:18 +0400, Sergei Meshveliani wrote:
> People, I have a couple of questions about general relation between
> _≤_ and _<_
> in the lib-0.7 standard library.
> 1. What is the most general situation in lib-0.7 under which these
> usual properties can be proved:
> x ≤ y iff x < y ⊎ x ≈ y (I),
> x < y -> ¬ y ≤ x (II)
> 2. For Nat,
> it is natural to derive (I) and (II) from DecTotalOrder,
> as a specialization of the above generic laws.
> But DecTotalOrder says nothing about _<_.
> Then, we are forced to derive (I) and (II) from the union of
> DecTotalOrder and StrictTotalOrder.
> Well, Data.Nat has decTotalOrder. But it is silent about
Sorry, I see now Data.Nat.Properties.strictTotalOrder
This withdraws the question 2.
The questions 1 and 3 remain.
More information about the Agda