Idris2Doc : HTTP.RequestErr

HTTP.RequestErr

(source)

Definitions

record RequestErr : Type
Totality: total
Visibility: public export
Constructor: 
RE : Bits16 -> String -> String -> String -> String -> RequestErr

Projections:
.details : RequestErr -> String
.error : RequestErr -> String
.message : RequestErr -> String
.path : RequestErr -> String
.status : RequestErr -> Bits16

Hints:
Eq RequestErr
FromJSON RequestErr
HTTPLocal => Interpolation RequestErr
Show RequestErr
ToJSON RequestErr
.status : RequestErr -> Bits16
Totality: total
Visibility: public export
status : RequestErr -> Bits16
Totality: total
Visibility: public export
.error : RequestErr -> String
Totality: total
Visibility: public export
error : RequestErr -> String
Totality: total
Visibility: public export
.message : RequestErr -> String
Totality: total
Visibility: public export
message : RequestErr -> String
Totality: total
Visibility: public export
.details : RequestErr -> String
Totality: total
Visibility: public export
details : RequestErr -> String
Totality: total
Visibility: public export
.path : RequestErr -> String
Totality: total
Visibility: public export
path : RequestErr -> String
Totality: total
Visibility: public export
requestErr : Status -> RequestErr
Totality: total
Visibility: export
requestErrMsg : String -> Status -> RequestErr
Totality: total
Visibility: export
requestErrDetails : Interpolation a => a -> Status -> RequestErr
Totality: total
Visibility: export