Idris2Doc : Control.WellFounded

Control.WellFounded

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

Implementations:
SizedNat
Sized (Lista)
(Sizeda, Sizedb) => Sized (a, b)
Smaller : Sizeda => a -> a -> Type
WellFounded : (a : Type) -> (a -> a -> Type) -> Type
Parameters: a, rel
Methods:
wellFounded : (x : a) -> Accessiblerelx
accInd : {0 P : a -> Type} -> ((x : a) -> ((y : a) -> relyx -> Py) -> Px) -> (z : a) -> (0 _ : Accessiblerelz) -> Pz
accRec : ((x : a) -> ((y : a) -> relyx -> b) -> b) -> (z : a) -> (0 _ : Accessiblerelz) -> b
size : Sizeda => a -> Nat
sizeAccessible : {auto {conArg:978} : Sizeda} -> (x : a) -> SizeAccessiblex
sizeInd : {auto {conArg:1033} : Sizeda} -> {0 P : a -> Type} -> ((x : a) -> ((y : a) -> Smalleryx -> Py) -> Px) -> (z : a) -> Pz
sizeRec : {auto {conArg:1071} : Sizeda} -> ((x : a) -> ((y : a) -> Smalleryx -> b) -> b) -> a -> b
wellFounded : WellFoundedarel => (x : a) -> Accessiblerelx
wfInd : {auto 0 _ : WellFoundedarel} -> {0 P : a -> Type} -> ((x : a) -> ((y : a) -> relyx -> Py) -> Px) -> (myz : a) -> Pmyz
wfRec : {auto 0 _ : WellFoundedarel} -> ((x : a) -> ((y : a) -> relyx -> b) -> b) -> a -> b