Idris2Doc : TyTTP.Core.Context

TyTTP.Core.Context

(source)

Reexports

import public Control.Monad.Trans

Definitions

record Context : Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type
Totality: total
Visibility: public export
Constructor: 
MkContext : Request me u v h1 a -> Response s h2 b -> Context me u v h1 s h2 a b

Projections:
.request : Context me u v h1 s h2 a b -> Request me u v h1 a
.response : Context me u v h1 s h2 a b -> Response s h2 b

Hints:
Bifunctor (Context me u v h1 s h2)
Functor (Context me u v h1 s h2 a)
.request : Context me u v h1 s h2 a b -> Request me u v h1 a
Visibility: public export
request : Context me u v h1 s h2 a b -> Request me u v h1 a
Visibility: public export
.response : Context me u v h1 s h2 a b -> Response s h2 b
Visibility: public export
response : Context me u v h1 s h2 a b -> Response s h2 b
Visibility: public export
(:>) : MonadTrans t => Monad m => ((a -> t m b) -> c) -> (a -> m b) -> c
Visibility: export
Fixity Declaration: infixr operator, level 0
(:>>) : MonadTrans t1 => MonadTrans t2 => Monad m => Monad (t1 m) => ((a -> t2 (t1 m) b) -> c) -> (a -> m b) -> c
Visibility: export
Fixity Declaration: infixr operator, level 0