Idris2Doc : Control.WellFounded

Control.WellFounded

data Accessible : (a -> a -> Type) -> a -> Type
  Totality: total
  Constructor: 
Access : ((y : a) -> rel y x -> Accessible rel y) -> Accessible rel x
SizeAccessible : Sized a => a -> Type
  Totality: total
interface Sized : Type -> Type
  Parameters: a
Constructor: MkSized
Methods:
  
size : a -> Nat

Implementations:
  
Sized Nat
  
Sized (List a)
  
(Sized a, Sized b) => Sized (a, b)
Smaller : Sized a => a -> a -> Type
  Totality: total
interface WellFounded : (a : Type) -> (a -> a -> Type) -> Type
  Parameters: a, rel
Methods:
  
wellFounded : (x : a) -> Accessible rel x

Implementation: 
WellFounded Nat LT
accInd : {0 P : a -> Type} -> ((x : a) -> ((y : a) -> rel y x -> P y) -> P x) -> (z : a) -> (0 _ : Accessible rel z) -> P z
  Totality: total
accRec : ((x : a) -> ((y : a) -> rel y x -> b) -> b) -> (z : a) -> (0 _ : Accessible rel z) -> b
  Totality: total
size : Sized a => a -> Nat
  Totality: total
sizeAccessible : {auto conArg : Sized a} -> (x : a) -> SizeAccessible x
  Totality: total
sizeInd : {auto conArg : Sized a} -> {0 P : a -> Type} -> ((x : a) -> ((y : a) -> Smaller y x -> P y) -> P x) -> (z : a) -> P z
  Totality: total
sizeRec : {auto conArg : Sized a} -> ((x : a) -> ((y : a) -> Smaller y x -> b) -> b) -> a -> b
  Totality: total
wellFounded : WellFounded a rel => (x : a) -> Accessible rel x
  Totality: total
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
  Totality: total
wfRec : {auto 0 _ : WellFounded a rel} -> ((x : a) -> ((y : a) -> rel y x -> b) -> b) -> a -> b
  Totality: total