
  0 | module HTTP.API.Endpoints
  1 | 
  2 | import public Data.List.Quantifiers
  3 | 
  4 | %default total
  5 | 
  6 | ||| A list of heterogeneous lists, used to describe the APIs of
  7 | ||| a webserver.
  8 | public export
  9 | data Endpoints : Type where
 10 |   Nil  : Endpoints
 11 |   (::) : {0 ts : List Type} -> HList ts -> Endpoints -> Endpoints
 12 | 
 13 | ||| Concatenates two APIs.
 14 | public export
 15 | (++) : Endpoints -> Endpoints -> Endpoints
 16 | (++) (a::as) bs = a :: (as ++ bs)
 17 | (++) []      bs = bs
 18 |