Idris2Doc : Control.WellFounded

Control.WellFounded

dataAccessible : (a -> a -> Type) -> a -> Type
Totality: total
Constructor: 
Access : ((y : a) -> relyx -> Accessiblerely) -> Accessiblerelx
SizeAccessible : Sizeda => a -> Type
Totality: total
interfaceSized : Type -> Type
Parameters: a
Constructor: MkSized
Methods:
size : a -> Nat

Implementations:
SizedNat
Sized (Lista)
(Sizeda, Sizedb) => Sized (a, b)
Smaller : Sizeda => a -> a -> Type
Totality: total
interfaceWellFounded : (a : Type) -> (a -> a -> Type) -> Type
Parameters: a, rel
Methods:
wellFounded : (x : a) -> Accessiblerelx

Implementation: 
WellFoundedNatLT
accInd : {0 P : a -> Type} -> ((x : a) -> ((y : a) -> relyx -> Py) -> Px) -> (z : a) -> (0 _ : Accessiblerelz) -> Pz
Totality: total
accRec : ((x : a) -> ((y : a) -> relyx -> b) -> b) -> (z : a) -> (0 _ : Accessiblerelz) -> b
Totality: total
size : Sizeda => a -> Nat
Totality: total
sizeAccessible : {autoconArg : Sizeda} -> (x : a) -> SizeAccessiblex
Totality: total
sizeInd : {autoconArg : Sizeda} -> {0 P : a -> Type} -> ((x : a) -> ((y : a) -> Smalleryx -> Py) -> Px) -> (z : a) -> Pz
Totality: total
sizeRec : {autoconArg : Sizeda} -> ((x : a) -> ((y : a) -> Smalleryx -> b) -> b) -> a -> b
Totality: total
wellFounded : WellFoundedarel => (x : a) -> Accessiblerelx
Totality: total
wfInd : {auto 0 _ : WellFoundedarel} -> {0 P : a -> Type} -> ((x : a) -> ((y : a) -> relyx -> Py) -> Px) -> (myz : a) -> Pmyz
Totality: total
wfRec : {auto 0 _ : WellFoundedarel} -> ((x : a) -> ((y : a) -> relyx -> b) -> b) -> a -> b
Totality: total