Idris2Doc : HTTP.Header.Types

HTTP.Header.Types

(source)
Definitions
data Parameter : Type
  Totality: total
  Visibility: public export
  Constructors:
  
P : String -> String -> Parameter
  
Q : Double -> Parameter

  Hints:
  
Eq Parameter
  
Show Parameter
0 Parameters : Type
  Totality: total
  Visibility: public export
parameter : String -> Parameters -> Maybe String
  Totality: total
  Visibility: export
weight : Parameters -> Double
  Totality: total
  Visibility: export
data MediaDesc : Type
  Totality: total
  Visibility: public export
  Constructors:
  
MDAny : MediaDesc
  
MDStar : String -> MediaDesc
  
MD : String -> String -> MediaDesc

  Hints:
  
Eq MediaDesc
  
Show MediaDesc
record MediaRange : Type
  Totality: total
  Visibility: public export
  Constructor: 
MR : MediaDesc -> Parameters -> MediaRange

  Projections:
  
.params : MediaRange -> Parameters
  
.type : MediaRange -> MediaDesc

  Hints:
  
Eq MediaRange
  
Show MediaRange
.type : MediaRange -> MediaDesc
  Totality: total
  Visibility: public export
type : MediaRange -> MediaDesc
  Totality: total
  Visibility: public export
.params : MediaRange -> Parameters
  Totality: total
  Visibility: public export
params : MediaRange -> Parameters
  Totality: total
  Visibility: public export
record MediaType : Type
  Totality: total
  Visibility: public export
  Constructor: 
MT : String -> String -> MediaType

  Projections:
  
.subtype : MediaType -> String
  
.type : MediaType -> String

  Hints:
  
Eq MediaType
  
Show MediaType
.type : MediaType -> String
  Totality: total
  Visibility: public export
type : MediaType -> String
  Totality: total
  Visibility: public export
.subtype : MediaType -> String
  Totality: total
  Visibility: public export
subtype : MediaType -> String
  Totality: total
  Visibility: public export
encodeMediaType : MediaType -> ByteString
  Totality: total
  Visibility: export
record ContentType : Type
  Totality: total
  Visibility: public export
  Constructor: 
CT : MediaType -> Parameters -> ContentType

  Projections:
  
.params : ContentType -> Parameters
  
.type : ContentType -> MediaType

  Hints:
  
Eq ContentType
  
Show ContentType
.type : ContentType -> MediaType
  Totality: total
  Visibility: public export
type : ContentType -> MediaType
  Totality: total
  Visibility: public export
.params : ContentType -> Parameters
  Totality: total
  Visibility: public export
params : ContentType -> Parameters
  Totality: total
  Visibility: public export
accepts : MediaDesc -> MediaType -> Bool
  Totality: total
  Visibility: export
0 MediaRanges : Type
  Totality: total
  Visibility: public export
record ContentDisp : Type
  Totality: total
  Visibility: public export
  Constructor: 
CD : String -> Parameters -> ContentDisp

  Projections:
  
.disp : ContentDisp -> String
  
.params : ContentDisp -> Parameters

  Hints:
  
Eq ContentDisp
  
Show ContentDisp
.disp : ContentDisp -> String
  Totality: total
  Visibility: public export
disp : ContentDisp -> String
  Totality: total
  Visibility: public export
.params : ContentDisp -> Parameters
  Totality: total
  Visibility: public export
params : ContentDisp -> Parameters
  Totality: total
  Visibility: public export
0 HeaderMap : Type
  Totality: total
  Visibility: public export