Idris2Doc : Collie.Core

Collie.Core

(source)
Reexports
import public Collie.Options.Domain
import public Collie.Options.Usual
import public Collie.Modifiers
import public Data.Record
import public Data.Record.SmartConstructors
import public Data.Vect
import public Data.DPair
import public Data.Magma
import public Syntax.WithProof
import public Decidable.Decidable
import public Decidable.Decidable.Extra1
Definitions
record Command : String -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCommand : String -> Fields Command -> Fields Modifier -> Arguments -> Command name

  Projections:
  
.arguments : Command name -> Arguments
  
.description : Command name -> String
  
.modifiers : Command name -> Fields Modifier
  
.subcommands : Command name -> Fields Command
.description : Command name -> String
  Totality: total
  Visibility: public export
description : Command name -> String
  Totality: total
  Visibility: public export
.subcommands : Command name -> Fields Command
  Totality: total
  Visibility: public export
subcommands : Command name -> Fields Command
  Totality: total
  Visibility: public export
.modifiers : Command name -> Fields Modifier
  Totality: total
  Visibility: public export
modifiers : Command name -> Fields Modifier
  Totality: total
  Visibility: public export
.arguments : Command name -> Arguments
  Totality: total
  Visibility: public export
arguments : Command name -> Arguments
  Totality: total
  Visibility: public export
basic : String -> Arguments -> Command cmdName
  Totality: total
  Visibility: public export
data Any : ((0 nm : String) -> Command nm -> Type) -> Command nm -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Here : p nm cmd -> Any p cmd
  
There : (pos : IsField c (cmd .subcommands)) -> Any p (snd (field pos)) -> Any p cmd
map : ((cmd : Command nm) -> p nm cmd -> q nm cmd) -> Any p cmd -> Any q cmd
  Totality: total
  Visibility: public export
traverse : Applicative m => ((cmd : Command nm) -> p nm cmd -> m (q nm cmd)) -> Any p cmd -> m (Any q cmd)
  Totality: total
  Visibility: public export
record ParsedCommandT : (Type -> Type) -> (Type -> Type) -> (0 nm : String) -> Command nm -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkParsedCommandT : ParsedModifiersT f g (cmd .modifiers) -> ParsedArgumentsT g (cmd .arguments) -> ParsedCommandT f g nm cmd

  Projections:
  
.arguments : ParsedCommandT f g nm cmd -> ParsedArgumentsT g (cmd .arguments)
  
.modifiers : ParsedCommandT f g nm cmd -> ParsedModifiersT f g (cmd .modifiers)
.modifiers : ParsedCommandT f g nm cmd -> ParsedModifiersT f g (cmd .modifiers)
  Totality: total
  Visibility: public export
modifiers : ParsedCommandT f g nm cmd -> ParsedModifiersT f g (cmd .modifiers)
  Totality: total
  Visibility: public export
.arguments : ParsedCommandT f g nm cmd -> ParsedArgumentsT g (cmd .arguments)
  Totality: total
  Visibility: public export
arguments : ParsedCommandT f g nm cmd -> ParsedArgumentsT g (cmd .arguments)
  Totality: total
  Visibility: public export
record ParsedCommand : (0 nm : String) -> Command nm -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkParsedCommand : ParsedModifiers (cmd .modifiers) -> ParsedArguments (cmd .arguments) -> ParsedCommand nm cmd

  Projections:
  
.arguments : ParsedCommand nm cmd -> ParsedArguments (cmd .arguments)
  
.modifiers : ParsedCommand nm cmd -> ParsedModifiers (cmd .modifiers)
.modifiers : ParsedCommand nm cmd -> ParsedModifiers (cmd .modifiers)
  Totality: total
  Visibility: public export
modifiers : ParsedCommand nm cmd -> ParsedModifiers (cmd .modifiers)
  Totality: total
  Visibility: public export
.arguments : ParsedCommand nm cmd -> ParsedArguments (cmd .arguments)
  Totality: total
  Visibility: public export
arguments : ParsedCommand nm cmd -> ParsedArguments (cmd .arguments)
  Totality: total
  Visibility: public export
defaulting : ParsedCommandT Maybe f nm cmd -> ParsedCommandT id f nm cmd
  Totality: total
  Visibility: public export
finalising : ParsedCommandT Maybe Maybe nm cmd -> Error (ParsedCommand nm cmd)
  Totality: total
  Visibility: public export
ParseTreeT : (Type -> Type) -> (Type -> Type) -> Command nm -> Type
  Totality: total
  Visibility: public export
ParseTree : Command nm -> Type
  Totality: total
  Visibility: public export
defaulting : ParseTreeT Maybe f cmd -> ParseTreeT id f cmd
  Totality: total
  Visibility: public export
finalising : ParseTreeT Maybe Maybe cmd -> Error (ParseTree cmd)
  Totality: total
  Visibility: public export
lookup : Any p c -> (nm : String ** Command nm)
  Totality: total
  Visibility: public export
.update : ParsedArgumentsT Maybe arg -> String -> Error (ParsedArgumentsT Maybe arg)
  Totality: total
  Visibility: public export
.parse : (args : Arguments) -> ParsedArgumentsT Maybe args -> List String -> Error (ParsedArgumentsT Maybe args)
  Totality: total
  Visibility: public export
initParsedCommand : ParsedCommandT Maybe Maybe nm cmd
  Totality: total
  Visibility: public export