Idris2Doc : Data.DPair

Data.DPair

Definitions

choice : {0p : a->b->Type} -> ((x : a) -> (b : b**pxb)) -> (f : a->b** (x : a) ->px (fx))
  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 export
choice : {0b : a->Type} -> {0p : (x : a) ->bx->Type} -> ((x : a) -> (y : bx**pxy)) -> (f : (x : a) ->bx** (x : a) ->px (fx))
  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 export
curry : {0p : a->Type} -> ((x : a**px) ->c) -> (x : a) ->px->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 export
uncurry : {0p : a->Type} -> ((x : a) ->px->c) -> (x : a**px) ->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 export
bimap : {0p : a->Type} -> {0q : b->Type} -> (f : (a->b)) -> (px->q (fx)) -> (x : a**px) -> (y : b**qy)
  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 export
recordExists : (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 : (0fst : type) ->thisfst->Existsthis

Projections:
0.fst : Existsthis->type
.snd : ({rec:0} : Existsthis) ->this (fst{rec:0})
0.fst : Existsthis->type
Totality: total
Visibility: public export
0fst : Existsthis->type
Totality: total
Visibility: public export
.snd : ({rec:0} : Existsthis) ->this (fst{rec:0})
Totality: total
Visibility: public export
snd : ({rec:0} : Existsthis) ->this (fst{rec:0})
Totality: total
Visibility: public export
curry : (Existsp->c) ->px->c
Totality: total
Visibility: public export
uncurry : (px->c) ->Existsp->c
Totality: total
Visibility: public export
evidenceInjectiveFst : Evidencexp=Evidenceyq->x=y
Totality: total
Visibility: export
evidenceInjectiveSnd : Evidencexp=Evidencexq->p=q
Totality: total
Visibility: export
bimap : (0f : (a->b)) -> (px->q (fx)) ->Existsp->Existsq
Totality: total
Visibility: public export
recordSubset : (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_ : predfst) ->Subsettypepred

Projections:
.fst : Subsettypepred->type
0.snd : ({rec:0} : Subsettypepred) ->pred (fst{rec:0})

Hints:
Eqtype=>Eq (Subsettypepred)
Ordtype=>Ord (Subsettypepred)
Showtype=>Show (Subsettypepred)
.fst : Subsettypepred->type
Totality: total
Visibility: public export
fst : Subsettypepred->type
Totality: total
Visibility: public export
0.snd : ({rec:0} : Subsettypepred) ->pred (fst{rec:0})
Totality: total
Visibility: public export
0snd : ({rec:0} : Subsettypepred) ->pred (fst{rec:0})
Totality: total
Visibility: public export
curry : (Subsetap->c) -> (x : a) -> (0_ : px) ->c
Totality: total
Visibility: public export
uncurry : ((x : a) -> (0_ : px) ->c) ->Subsetap->c
Totality: total
Visibility: public export
elementInjectiveFst : Elementxp=Elementyq->x=y
Totality: total
Visibility: export
elementInjectiveSnd : Elementxp=Elementxq->p=q
Totality: total
Visibility: export
bimap : (f : (a->b)) -> (0_ : (px->q (fx))) ->Subsetap->Subsetbq
Totality: total
Visibility: public export