HTTP.API.Path

Definitions

data Part : Type

  Single part in a URI path.
  
  This matches either a specific string or one or more variables
  stored at the given position in the path.

Totality: total
Visibility: public export
Constructors:

PStr : String -> Part

PTill : String -> Part

Capture : (0 _ : Type) -> Part

Hint: 

FromString Part

0 PartsTypes : List Part -> List Type

  Computes the list of types captured by a URI path description.

Totality: total
Visibility: public export

record ReqPath : Type

  Describes a pattern for matching and extracting
  values for the path of the request URI.

Totality: total
Visibility: public export
Constructor: 

Path : List Part -> ReqPath

Projection: 

.parts : ReqPath -> List Part

.parts : ReqPath -> List Part

Totality: total
Visibility: public export

parts : ReqPath -> List Part

Totality: total
Visibility: public export