[Agda] Nat arithmetic properties

[Ulf Norell]

On Thu, Sep 22, 2016 at 10:08 PM, Sergei Meshveliani <mechvel at botik.ru>
 wrote:

> Another reason for necessity of n-ary provable arithmetic:
>
>   _≤?_  of Data.Nat.decTotalOrder  is slow.
>
> Probably this is because it is not built-in
> (and how can it? assuming that the result may contain a proof made of
> many certain constructors).


You should use the _≤″_ ordering [1] instead. It has constant size
representation
of inequality proofs.

/ Ulf

[1]
https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Base.agda#L72
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160922/d4bb117a/attachment.html