[Agda] `accessible' for ℕ

[Sergei Meshveliani]

On Fri, 2018-08-31 at 14:34 +0200, Ulf Norell wrote:
> I believe it's simply Induction.Nat.<-wellFounded.
> 

Thank you. It works this:

  <-acc {n} = Induction.Nat.<-wellFounded n



> 
> 
> 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