TyTTP.URL.Path

(source)

Reexports

import public Data.Either

Definitions

data ParseError : Type

Totality: total
Visibility: public export
Constructors:

EmptyPattern : ParseError
ParamShouldFollowALiteral : String -> List Elem -> ParseError
RestShouldFollowALiteral : String -> List Elem -> ParseError
ParamAlreadyDefined : String -> List Elem -> ParseError
ParamEmpty : String -> List Elem -> ParseError
UnclosedParam : String -> List Elem -> ParseError
InvalidStartCharInParam : Char -> List Elem -> ParseError
InvalidCharInParam : Char -> List Elem -> ParseError
RestShouldBeLast : String -> List Elem -> ParseError

data ParsedPattern : (0 _ : String) -> Type

Totality: total
Visibility: export
Constructor:

MkParsedPattern : List Elem -> ParsedPattern s

parse : (s : String) -> Either ParseError (ParsedPattern s)

Totality: total
Visibility: public export

record Path : Type

Totality: total
Visibility: public export
Constructor:

MkPath : String -> List (String, String) -> String -> Path

Projections:

.params : Path -> List (String, String)
.raw : Path -> String
.rest : Path -> String

.raw : Path -> String

Totality: total
Visibility: public export

raw : Path -> String

Totality: total
Visibility: public export

.params : Path -> List (String, String)

Totality: total
Visibility: public export

params : Path -> List (String, String)

Totality: total
Visibility: public export

.rest : Path -> String

Totality: total
Visibility: public export

rest : Path -> String

Totality: total
Visibility: public export

pattern : Monad m => Alternative m => (str : String) -> {auto 0 _ : IsRight (parse str)} -> (Context me (URL auth Path s) v h1 st h2 a b -> m (Context me' (URL auth Path s) v' h1' st' h2' a' b')) -> Context me (URL auth String s) v h1 st h2 a b -> m (Context me' (URL auth String s) v' h1' st' h2' a' b')

Totality: total
Visibility: export