Idris2Doc : HTTP.Parser.Header

HTTP.Parser.Header

(source)
Definitions
dayname : RExp True
  Totality: total
  Visibility: public export
daynameL : RExp True
  Totality: total
  Visibility: export
second : RExp True
  Totality: total
  Visibility: public export
minute : RExp True
  Totality: total
  Visibility: public export
hour : RExp True
  Totality: total
  Visibility: public export
timeOfDay : RExp True
  Totality: total
  Visibility: public export
month : RExp True
  Totality: total
  Visibility: public export
year : RExp True
  Totality: total
  Visibility: public export
qvalue : RExp True
  Totality: total
  Visibility: export
data HState : List Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
HMap : HState [HeaderMap]
  
HNam : HState [String]
  
HPar : HState [SnocList Parameter]
  
HParS : HState [Void]
  
HParN : HState [String, SnocList Parameter]
  
HParQ : HState [Void]
  
HVal1 : HState []
  
HVal : HState [String]
  
HAcc : HState [SnocList MediaRange]
  
HAccD : HState [MediaDesc, SnocList MediaRange]
  
HField : HState [Void]
  
HStr : HState [Void]
  
HNat : HState [Nat]
  
HMT : HState []
  
HMT1 : HState [MediaType]
  
HCD : HState []
  
HCD1 : HState [String]
  
HEnd : HState [Void]
  
HErr : HState []

  Hints:
  
Cast (HState ts) (Index HSz)
  
Show (HState {arg:8988})
data HRes : HState ts -> Stack False HState ts -> Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
RMap : HRes HMap [empty] HeaderMap
  
RAcc : HRes HAcc [[<]] (List MediaRange)
  
RConL : HRes HNat [0] Nat
  
RConT : HRes HMT [] ContentType
  
RConD : HRes HCD [] ContentDisp
  
RVal : HRes HVal1 [] String
0 SK : Type -> Type
  Totality: total
  Visibility: public export
header : HRes st x t -> P1 q (BoundedErr Void) t
  Totality: total
  Visibility: public export
headerMay : HRes st x t -> ByteString -> Maybe t
  Totality: total
  Visibility: export
testHeader : HRes st x v -> Show v => String -> IO ()
  Totality: total
  Visibility: export