<div dir="ltr"><div>I believe it's simply Induction.Nat.<-wellFounded.</div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr">On Fri, Aug 31, 2018 at 2:30 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This is on Standard library. <br>
<br>
Please, how to extract<br>
               <-acc : {n : ℕ} →Acc _<_<br>
<br>
from  Induction.Nat ?<br>
<br>
I program it by<br>
<br>
  <-acc {0}      =  acc (\_ ())<br>
  <-acc {suc n}  with <-acc {n}<br>
  ...            | acc wf = acc f<br>
                            where ...,<br>
<br>
but probably it can be somehow imported from Induction.Nat.<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>