Idris2Doc : Pipeline.Basic

Pipeline.Basic

(source)
Reexports
import public Data.Vect
import public Data.Vect.Utils
import public Data.Vect.Quantifiers
Definitions
Pipeline : Nat -> Type
  Visibility: public export
Fn : Type -> Type -> Type
  Visibility: public export
KleisliFn : (Type -> Type) -> Type -> Type -> Type
  Visibility: public export
Impl : Pipeline (2 + n) -> Type
  Visibility: public export
Run : (p : Pipeline (2 + n)) -> Impl p -> head p -> last p
  Visibility: export
RunTrace : (p : Pipeline (2 + n)) -> All Show p => Impl p -> head p -> last p
  Visibility: export
ImplM : Pipeline (2 + n) -> Type
  Visibility: public export
RunM : Monad m => (p : Pipeline (2 + n)) -> ImplM p -> head p -> m (last p)
  Visibility: export
RunTraceM : Monad m => (p : Pipeline (2 + n)) -> All Show p => ImplM p -> head p -> m (last p)
  Visibility: export