Collie.Options.Domain

Definitions

data Domain : Type

Totality: total
Visibility: public export
Constructors:

Some : Type -> Domain

ALot : RawMagma -> Domain

elimDomain : {p : Domain -> Type} -> ((d : Type) -> p (Some d)) -> ((ds : RawMagma) -> p (ALot ds)) -> (d : Domain) -> p d

Totality: total
Visibility: public export

Carrier : Domain -> Type

Totality: total
Visibility: public export

Parser : Domain -> Type

Totality: total
Visibility: public export

record Arguments : Type

Totality: total
Visibility: public export
Constructor: 

MkArguments : Bool -> (domain : Domain) -> Parser domain -> Arguments

Projections:

.domain : Arguments -> Domain

.rawParser : ({rec:0} : Arguments) -> Parser (domain {rec:0})

.required : Arguments -> Bool

.required : Arguments -> Bool

Totality: total
Visibility: public export

required : Arguments -> Bool

Totality: total
Visibility: public export

.domain : Arguments -> Domain

Totality: total
Visibility: public export

domain : Arguments -> Domain

Totality: total
Visibility: public export

.rawParser : ({rec:0} : Arguments) -> Parser (domain {rec:0})

Totality: total
Visibility: public export

rawParser : ({rec:0} : Arguments) -> Parser (domain {rec:0})

Totality: total
Visibility: public export

.parser : (arg : Arguments) -> String -> Error (Carrier (arg .domain))

Totality: total
Visibility: public export

ParsedArgumentsT : (Type -> Type) -> Arguments -> Type

Totality: total
Visibility: public export

ParsedArguments : Arguments -> Type

Totality: total
Visibility: public export