Idris2Doc : TyTTP.URL.Definition

TyTTP.URL.Definition

(source)
Definitions
data Scheme : Type
  Totality: total
  Visibility: public export
  Constructors:
  
HTTP : Scheme
  
HTTPS : Scheme
  
OtherScheme : String -> Scheme

  Hint: 
Show Scheme
parse : String -> Scheme
  Visibility: export
record URL : Type -> Type -> Type -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkURL : Maybe Scheme -> Maybe a -> p -> s -> URL a p s

  Projections:
  
.authority : URL a p s -> Maybe a
  
.path : URL a p s -> p
  
.scheme : URL a p s -> Maybe Scheme
  
.search : URL a p s -> s
.scheme : URL a p s -> Maybe Scheme
  Visibility: public export
scheme : URL a p s -> Maybe Scheme
  Visibility: public export
.authority : URL a p s -> Maybe a
  Visibility: public export
authority : URL a p s -> Maybe a
  Visibility: public export
.path : URL a p s -> p
  Visibility: public export
path : URL a p s -> p
  Visibility: public export
.search : URL a p s -> s
  Visibility: public export
search : URL a p s -> s
  Visibility: public export