Idris2Doc : HTTP.Status

HTTP.Status

(source)
Definitions
record Status : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkStatus : Bits16 -> String -> Status

  Projections:
  
.code : Status -> Bits16
  
.message : Status -> String

  Hints:
  
Cast Status ByteString
  
Interpolation Status
.code : Status -> Bits16
  Totality: total
  Visibility: public export
code : Status -> Bits16
  Totality: total
  Visibility: public export
.message : Status -> String
  Totality: total
  Visibility: public export
message : Status -> String
  Totality: total
  Visibility: public export
ok200 : Status
  Totality: total
  Visibility: export
created201 : Status
  Totality: total
  Visibility: export
accepted202 : Status
  Totality: total
  Visibility: export
noContent204 : Status
  Totality: total
  Visibility: export
badRequest400 : Status
  Totality: total
  Visibility: export
unauthorized401 : Status
  Totality: total
  Visibility: export
forbidden403 : Status
  Totality: total
  Visibility: export
notFound404 : Status
  Totality: total
  Visibility: export
methodNotAllowed405 : Status
  Totality: total
  Visibility: export
notAcceptable406 : Status
  Totality: total
  Visibility: export
conflict409 : Status
  Totality: total
  Visibility: export
contentTooLarge413 : Status
  Totality: total
  Visibility: export
unsupportedMediaType415 : Status
  Totality: total
  Visibility: export
requestHeaderFieldsTooLarge431 : Status
  Totality: total
  Visibility: export
internalServerError500 : Status
  Totality: total
  Visibility: export
notImplemented501 : Status
  Totality: total
  Visibility: export
insufficientStorage507 : Status
  Totality: total
  Visibility: export
networkAuthenticationRequired511 : Status
  Totality: total
  Visibility: export