Collie.Modifiers

Reexports

Definitions

(::=) : {0 a : String -> Type} -> (nm : String) -> a nm -> (nm : String ** a nm)

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 1

Flag : Fields (const Type)

Totality: total
Visibility: public export

Option : Fields (const Type)

Totality: total
Visibility: public export

data Modifier : String -> Type

Totality: total
Visibility: public export
Constructors:

MkFlag : Record snd Flag -> Modifier nm

MkOption : Record snd Option -> Modifier nm

flag : String -> {default False _ : Bool} -> Modifier nm

Totality: total
Visibility: public export

option : String -> Arguments -> Modifier nm

Totality: total
Visibility: public export

ParsedModifierT : (Type -> Type) -> (Type -> Type) -> Modifier nm -> Type

Totality: total
Visibility: public export

ParsedModifier : Modifier nm -> Type

Totality: total
Visibility: public export

ParsedModifiersT : (Type -> Type) -> (Type -> Type) -> Fields Modifier -> Type

Totality: total
Visibility: public export

ParsedModifiers : Fields Modifier -> Type

Totality: total
Visibility: public export

updateModifier : ParsedModifierT id id mod -> ParsedModifierT Maybe Maybe mod -> Error (ParsedModifierT Maybe Maybe mod)

Totality: total
Visibility: public export

.update : ParsedModifiersT Maybe Maybe mods -> (pos : Any p mods) -> ParsedModifierT id id (snd (field pos)) -> Error (ParsedModifiersT Maybe Maybe mods)

Totality: total
Visibility: public export

defaulting : ParsedModifiersT Maybe f mods -> ParsedModifiersT id f mods

  All the flags have a default value. If no value has been set then use
  that default instead.

Totality: total
Visibility: public export

finalising : Lazy ErrorMsg -> (args : Arguments) -> ParsedArgumentsT Maybe args -> Error (ParsedArguments args)

Totality: total
Visibility: public export

finalising : (mod : Modifier nm) -> ParsedModifierT Maybe Maybe mod -> Error (ParsedModifier mod)

Totality: total
Visibility: public export

finalising : ParsedModifiersT Maybe Maybe mods -> Error (ParsedModifiers mods)

  Setting the flags to their default value and ensuring that the required
  options are passed.

Totality: total
Visibility: public export

initNothing : ParsedModifiersT Maybe Maybe flds

Totality: total
Visibility: public export