<div dir="ltr">On Thu, Sep 22, 2016 at 10:08 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Another reason for necessity of n-ary provable arithmetic:<br><br>  _≤?_  of Data.Nat.decTotalOrder  is slow.<br><br>Probably this is because it is not built-in<br>(and how can it? assuming that the result may contain a proof made of<br>many certain constructors).</blockquote><div> </div>You <font color="#000000" face="arial, helvetica, sans-serif">should use the <span style="white-space:pre">_≤″_ ordering [1] instead. It has constant size representation</span></font><div><font color="#000000" face="arial, helvetica, sans-serif"><span style="white-space:pre">of inequality proofs.<br></span></font><div><span style="white-space:pre"><font color="#000000" face="arial, helvetica, sans-serif"><br></font></span></div><div><span style="white-space:pre"><font color="#000000" face="arial, helvetica, sans-serif">/ Ulf</font></span></div><div><span style="white-space:pre"><font color="#000000" face="arial, helvetica, sans-serif"><br></font></span></div><div><font color="#000000" face="arial, helvetica, sans-serif"><span style="white-space:pre">[1] <a href="https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Base.agda#L72">https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Base.agda#L72</a></span></font></div></div><div><br></div></div>