choice : {0 p : a -> b -> Type} -> ((x : a) -> (b : b ** p x b)) -> (f : a -> b ** (x : a) -> p x (f x)) Constructive choice: a function producing pairs of a value and a proof
can be split into a function producing a value and a family of proofs
for the images of that function.
Totality: total
Visibility: public exportchoice : {0 b : a -> Type} -> {0 p : (x : a) -> b x -> Type} -> ((x : a) -> (y : b x ** p x y)) -> (f : (x : a) -> b x ** (x : a) -> p x (f x)) Constructive choice: a function producing pairs of a value and a proof
can be split into a function producing a value and a family of proofs
for the images of that function.
Totality: total
Visibility: public exportcurry : {0 p : a -> Type} -> ((x : a ** p x) -> c) -> (x : a) -> p x -> c A function taking a pair of a value and a proof as an argument can be turned
into a function taking a value and a proof as two separate arguments.
Use `uncurry` to go in the other direction
Totality: total
Visibility: public exportuncurry : {0 p : a -> Type} -> ((x : a) -> p x -> c) -> (x : a ** p x) -> c A function taking a value and a proof as two separates arguments can be turned
into a function taking a pair of that value and its proof as a single argument.
Use `curry` to go in the other direction.
Totality: total
Visibility: public exportbimap : {0 p : a -> Type} -> {0 q : b -> Type} -> (f : (a -> b)) -> (p x -> q (f x)) -> (x : a ** p x) -> (y : b ** q y) Given a function on values and a family of proofs that this function takes
p-respecting inputs to q-respecting outputs,
we can turn: a pair of a value and a proof it is p-respecting
into: a pair of a value and a proof it is q-respecting
Totality: total
Visibility: public exportrecord Exists : (type -> Type) -> Type A dependent pair in which the first field (witness) should be
erased at runtime.
We can use `Exists` to construct dependent types in which the
type-level value is erased at runtime but used at compile time.
This type-level value could represent, for instance, a value
required for an intrinsic invariant required as part of the
dependent type's representation.
@type The type of the type-level value in the proof.
@this The dependent type that requires an instance of `type`.
Totality: total
Visibility: public export
Constructor: Evidence : (0 fst : type) -> this fst -> Exists this
Projections:
0 .fst : Exists this -> type.snd : ({rec:0} : Exists this) -> this (fst {rec:0})
0 .fst : Exists this -> type- Totality: total
Visibility: public export 0 fst : Exists this -> type- Totality: total
Visibility: public export .snd : ({rec:0} : Exists this) -> this (fst {rec:0})- Totality: total
Visibility: public export snd : ({rec:0} : Exists this) -> this (fst {rec:0})- Totality: total
Visibility: public export curry : (Exists p -> c) -> p x -> c- Totality: total
Visibility: public export uncurry : (p x -> c) -> Exists p -> c- Totality: total
Visibility: public export evidenceInjectiveFst : Evidence x p = Evidence y q -> x = y- Totality: total
Visibility: export evidenceInjectiveSnd : Evidence x p = Evidence x q -> p = q- Totality: total
Visibility: export bimap : (0 f : (a -> b)) -> (p x -> q (f x)) -> Exists p -> Exists q- Totality: total
Visibility: public export record Subset : (type : Type) -> (type -> Type) -> Type A dependent pair in which the second field (evidence) should not
be required at runtime.
We can use `Subset` to provide extrinsic invariants about a
value and know that these invariants are erased at
runtime but used at compile time.
@type The type-level value's type.
@pred The dependent type that requires an instance of `type`.
Totality: total
Visibility: public export
Constructor: Element : (fst : type) -> (0 _ : pred fst) -> Subset type pred
Projections:
.fst : Subset type pred -> type0 .snd : ({rec:0} : Subset type pred) -> pred (fst {rec:0})
Hints:
Eq type => Eq (Subset type pred)Ord type => Ord (Subset type pred)Show type => Show (Subset type pred)
.fst : Subset type pred -> type- Totality: total
Visibility: public export fst : Subset type pred -> type- Totality: total
Visibility: public export 0 .snd : ({rec:0} : Subset type pred) -> pred (fst {rec:0})- Totality: total
Visibility: public export 0 snd : ({rec:0} : Subset type pred) -> pred (fst {rec:0})- Totality: total
Visibility: public export curry : (Subset a p -> c) -> (x : a) -> (0 _ : p x) -> c- Totality: total
Visibility: public export uncurry : ((x : a) -> (0 _ : p x) -> c) -> Subset a p -> c- Totality: total
Visibility: public export elementInjectiveFst : Element x p = Element y q -> x = y- Totality: total
Visibility: export elementInjectiveSnd : Element x p = Element x q -> p = q- Totality: total
Visibility: export bimap : (f : (a -> b)) -> (0 _ : (p x -> q (f x))) -> Subset a p -> Subset b q- Totality: total
Visibility: public export