Idris2Doc : HTTP.API.Endpoints

HTTP.API.Endpoints

(source)
Reexports
import public Data.List.Quantifiers
Definitions
data Endpoints : Type
  A list of heterogeneous lists, used to describe the APIs of
  a webserver.

  Totality: total
  Visibility: public export
  Constructors:
  
Nil : Endpoints
  
(::) : HList ts -> Endpoints -> Endpoints
(++) : Endpoints -> Endpoints -> Endpoints
  Concatenates two APIs.

  Totality: total
  Visibility: public export
  Fixity Declaration: infixr operator, level 7