Idris2Doc : Pipeline.Dependent

Pipeline.Dependent

(source)
Reexports
import public Data.Telescope.Telescope
Definitions
head : Telescope (S n) -> Type
  Visibility: public export
tail : (xs : Telescope (S n)) -> head xs -> Telescope n
  Visibility: public export
record DContPair' : Type -> (y : Type) -> (y -> Type) -> Type
  Totality: total
  Visibility: public export
  Constructor: 
(|>>>) : x -> ((v : y) -> f v) -> DContPair' x y f

  Projections:
  
.cont : DContPair' x y f -> (v : y) -> f v
  
.fst : DContPair' x y f -> x
.fst : DContPair' x y f -> x
  Visibility: public export
fst : DContPair' x y f -> x
  Visibility: public export
.cont : DContPair' x y f -> (v : y) -> f v
  Visibility: public export
cont : DContPair' x y f -> (v : y) -> f v
  Visibility: public export
DContPair : (x : Type) -> (x -> Type) -> Type
  Visibility: public export
DContPairM : (Type -> Type) -> (x : Type) -> (x -> Type) -> Type
  Visibility: public export
HasShow : Telescope xs -> Type
  Visibility: public export
ToSigma : Telescope n -> Type
  Visibility: public export
ToImpl : Telescope n -> Type
  Visibility: public export
RunDep : (xs : Telescope (S (S n))) -> ToImpl xs -> (val : head xs) -> Environment (tail xs val)
  How to run the implementation of a telescope and obtain a
  sigma-types with all the intermediate results

  Visibility: export
RunTraceDep : (xs : Telescope (S (S n))) -> HasShow xs => ToImpl xs -> (val : head xs) -> Environment (tail xs val)
  How to run the implementation of a telescope and obtain a
  sigma-types with all the intermediate results

  Visibility: export
ToSigmaM : (m : (Type -> Type)) -> Monad m => Telescope n -> Type
  Visibility: public export
ToImplM : (m : (Type -> Type)) -> Monad m => Telescope n -> Type
  Visibility: public export
RunDepM : (m : (Type -> Type)) -> {auto inst : Monad m} -> (xs : Telescope (S (S n))) -> ToImplM xs -> (val : head xs) -> m (Environment (tail xs val))
  How to run the implementation of a telescope and obtain a
  sigma-types with all the intermediate results

  Visibility: export
RunTraceDepM : (m : (Type -> Type)) -> {auto inst : Monad m} -> (xs : Telescope (S (S n))) -> HasShow xs => ToImplM xs -> (val : head xs) -> m (Environment (tail xs val))
  Visibility: export