Idris2Doc : Control.WellFounded

Control.WellFounded

```Defines well-founded induction and recursion.

Induction is way to consume elements of recursive types where each step of
Normally, induction is structural: the previous steps are the children of
the current element.
any value that is less than the current element, based on a relation.

Well-founded induction is implemented in terms of accessibility: an element
is accessible (with respect to a given relation) if every element less than
it is also accessible. This can only terminate at minimum elements.

This corresponds to the idea that for a computation to terminate, there
must be a finite path to an element from which there is no way to recurse.

Many instances of well-founded induction are actually induction over
natural numbers that are derived from the elements being inducted over. For
this purpose, the `Sized` interface and related functions are provided.
```

Definitions

`data Accessible : (a -> a -> Type) -> a -> Type`
`  A value is accessible if everything smaller than it is also accessible.`

Totality: total
Visibility: public export
Constructor:
`Access : ((y : a) -> rel y x -> Accessible rel y) -> Accessible rel x`
`interface WellFounded : (a : Type) -> (a -> a -> Type) -> Type`
`  A relation is well-founded if every element is accessible.`

Parameters: a, rel
Methods:
`wellFounded : (x : a) -> Accessible rel x`

Implementation:
`WellFounded Nat LT`
`wellFounded : WellFounded a rel => (x : a) -> Accessible rel x`
Totality: total
Visibility: public export
`accRec : ((x : a) -> ((y : a) -> rel y x -> b) -> b) -> (z : a) -> (0 _ : Accessible rel z) -> b`
`  Simply-typed recursion based on accessibility.    The recursive step for an element has access to all elements smaller than  it. The recursion will therefore halt when it reaches a minimum element.    This may sometimes improve type-inference, compared to `accInd`.`

Totality: total
Visibility: export
`accInd : {0 P : a -> Type} -> ((x : a) -> ((y : a) -> rel y x -> P y) -> P x) -> (z : a) -> (0 _ : Accessible rel z) -> P z`
`  Depedently-typed induction based on accessibility.    The recursive step for an element has access to all elements smaller than  it. The recursion will therefore halt when it reaches a minimum element.`

Totality: total
Visibility: export
`accIndProp : {0 P : a -> Type} -> (step : ((x : a) -> ((y : a) -> rel y x -> P y) -> P x)) -> {0 RP : (x : a) -> P x -> Type} -> ((x : a) -> (f : ((y : a) -> rel y x -> P y)) -> ((y : a) -> (isRel : rel y x) -> RP y (f y isRel)) -> RP x (step x f)) -> (z : a) -> (0 acc : Accessible rel z) -> RP z (accInd step z acc)`
`  Depedently-typed induction for creating extrinsic proofs on results of `accInd`.`

Totality: total
Visibility: export
`wfRec : {auto 0 _ : WellFounded a rel} -> ((x : a) -> ((y : a) -> rel y x -> b) -> b) -> a -> b`
`  Simply-typed recursion based on well-founded-ness.    This is `accRec` applied to accessibility derived from a `WellFounded`  instance.`

Totality: total
Visibility: export
`wfInd : {auto 0 _ : WellFounded a rel} -> {0 P : a -> Type} -> ((x : a) -> ((y : a) -> rel y x -> P y) -> P x) -> (myz : a) -> P myz`
`  Depedently-typed induction based on well-founded-ness.    This is `accInd` applied to accessibility derived from a `WellFounded`  instance.`

Totality: total
Visibility: export
`wfIndProp : {auto 0 {conArg:1388} : WellFounded a rel} -> {0 P : a -> Type} -> (step : ((x : a) -> ((y : a) -> rel y x -> P y) -> P x)) -> {0 RP : (x : a) -> P x -> Type} -> ((x : a) -> (f : ((y : a) -> rel y x -> P y)) -> ((y : a) -> (isRel : rel y x) -> RP y (f y isRel)) -> RP x (step x f)) -> (myz : a) -> RP myz (wfInd step myz)`
`  Depedently-typed induction for creating extrinsic proofs on results of `wfInd`.`

Totality: total
Visibility: export
`interface Sized : Type -> Type`
`  Types that have a concept of size. The size must be a natural number.`

Parameters: a
Constructor:
`MkSized`

Methods:
`size : a -> Nat`

Implementations:
`Sized Nat`
`Sized (List a)`
`(Sized a, Sized b) => Sized (a, b)`
`size : Sized a => a -> Nat`
Totality: total
Visibility: public export
`Smaller : Sized a => a -> a -> Type`
`  A relation based on the size of the values.`

Totality: total
Visibility: public export
`SizeAccessible : Sized a => a -> Type`
`  Values that are accessible based on their size.`

Totality: total
Visibility: public export
`sizeAccessible : {auto {conArg:1594} : Sized a} -> (x : a) -> SizeAccessible x`
`  Any value of a sized type is accessible, since naturals are well-founded.`

Totality: total
Visibility: export
`sizeInd : {auto {conArg:1659} : Sized a} -> {0 P : a -> Type} -> ((x : a) -> ((y : a) -> Smaller y x -> P y) -> P x) -> (z : a) -> P z`
`  Depedently-typed induction based on the size of values.    This is `accInd` applied to accessibility derived from size.`

Totality: total
Visibility: export
`sizeRec : {auto {conArg:1720} : Sized a} -> ((x : a) -> ((y : a) -> Smaller y x -> b) -> b) -> a -> b`
`  Simply-typed recursion based on the size of values.    This is `recInd` applied to accessibility derived from size.`

Totality: total
Visibility: export