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: exportaccInd : {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: exportaccIndProp : {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: exportwfRec : {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: exportwfInd : {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: exportwfIndProp : {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: exportinterface 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 exportSizeAccessible : Sized a => a -> Type
Values that are accessible based on their size.
Totality: total
Visibility: public exportsizeAccessible : {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: exportsizeInd : {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: exportsizeRec : {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