[Agda] `accessible' for ℕ

[Ulf Norell]

I believe it's simply Induction.Nat.<-wellFounded.

/ Ulf

On Fri, Aug 31, 2018 at 2:30 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> This is on Standard library.
>
> Please, how to extract
>                <-acc : {n : ℕ} →Acc _<_
>
> from  Induction.Nat ?
>
> I program it by
>
>   <-acc {0}      =  acc (\_ ())
>   <-acc {suc n}  with <-acc {n}
>   ...            | acc wf = acc f
>                             where ...,
>
> but probably it can be somehow imported from Induction.Nat.
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180831/f96f12df/attachment.html>