[Agda] `accessible' for ℕ

[Sergei Meshveliani]

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

[Ulf Norell]

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

/ Ulf

Post by Sergei Meshveliani
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
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by Ulf Norell
I believe it's simply Induction.Nat.<-wellFounded.

Thank you. It works this:

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

Post by Ulf Norell
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
https://lists.chalmers.se/mailman/listinfo/agda