Idris2Doc : HTTP.RequestErr

HTTP.RequestErr

(source)

Definitions

recordRequestErr : 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:
EqRequestErr
FromJSONRequestErr
InterpolationRequestErr
ShowRequestErr
ToJSONRequestErr
.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 : Interpolationa=>a->Status->RequestErr
Totality: total
Visibility: export