0 | module TyTTP.Core.Response 1 | 2 | public export 3 | record Response s h a where 4 | constructor MkResponse 5 | status : s 6 | headers : h 7 | body : a 8 | 9 | export 10 | Functor (Response s h) where 11 | map f res = { body $= f } res 12 | 13 |