
  0 | module TyTTP.Core.Request
  1 | 
  2 | public export
  3 | record Request m u v h a where
  4 |   constructor MkRequest
  5 |   method : m
  6 |   url : u
  7 |   version : v
  8 |   headers : h
  9 |   body : a
 10 | 
 11 | export
 12 | Functor (Request m u v h) where
 13 |   map f req = { body $= f } req
 14 | 
 15 |