Idris2Doc : TyTTP.Core.Request
Definitions
record Request : Type -> Type -> Type -> Type -> Type -> Type- Totality: total
Visibility: public export
Constructor: MkRequest : m -> u -> v -> h -> a -> Request m u v h a
Projections:
.body : Request m u v h a -> a .method : Request m u v h a -> m .url : Request m u v h a -> u .version : Request m u v h a -> v
Hint: Functor (Request m u v h)
.method : Request m u v h a -> m- Visibility: public export
method : Request m u v h a -> m- Visibility: public export
.url : Request m u v h a -> u- Visibility: public export
url : Request m u v h a -> u- Visibility: public export
.version : Request m u v h a -> v- Visibility: public export
version : Request m u v h a -> v- Visibility: public export
- Visibility: public export
- Visibility: public export
.body : Request m u v h a -> a- Visibility: public export
body : Request m u v h a -> a- Visibility: public export