Idris2Doc : Pack.CmdLn.Types

Pack.CmdLn.Types

(source)
Definitions
data QueryMode : Type
  Mode used for querying the package collection:
  By package name, by dependency, or by module name.

  Totality: total
  Visibility: public export
  Constructors:
  
PkgName : QueryMode
  
Dependency : QueryMode
  
Module : QueryMode
record PkgQuery : Type
  A query to be run against the package collection

  Totality: total
  Visibility: public export
  Constructor: 
MkQ : QueryMode -> String -> PkgQuery

  Projections:
  
.mode : PkgQuery -> QueryMode
  
.query : PkgQuery -> String

  Hint: 
Arg PkgQuery
.mode : PkgQuery -> QueryMode
  Totality: total
  Visibility: public export
mode : PkgQuery -> QueryMode
  Totality: total
  Visibility: public export
.query : PkgQuery -> String
  Totality: total
  Visibility: public export
query : PkgQuery -> String
  Totality: total
  Visibility: public export
record FuzzyQuery : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkFQ : List PkgName -> String -> FuzzyQuery

  Projections:
  
.pkgs : FuzzyQuery -> List PkgName
  
.query : FuzzyQuery -> String

  Hint: 
Arg FuzzyQuery
.pkgs : FuzzyQuery -> List PkgName
  Totality: total
  Visibility: public export
pkgs : FuzzyQuery -> List PkgName
  Totality: total
  Visibility: public export
.query : FuzzyQuery -> String
  Totality: total
  Visibility: public export
query : FuzzyQuery -> String
  Totality: total
  Visibility: public export
data TrivialCmd : Type
  Trivial Commands accepted by *pack*. These commands do not require
  information about pack's configuration on the system.

  Totality: total
  Visibility: public export
  Constructor: 
CompletionScript : TrivialCmd

  Hint: 
Arg TrivialCmd
data ConfiguredCmd : Type
  Configured Commands accepted by *pack*. These commands require information
  about pack's configuration on the system.

  Totality: total
  Visibility: public export
  Constructors:
  
Build : ConfiguredCmd
  
BuildDeps : ConfiguredCmd
  
Typecheck : ConfiguredCmd
  
Clean : ConfiguredCmd
  
CleanBuild : ConfiguredCmd
  
Repl : ConfiguredCmd
  
Exec : ConfiguredCmd
  
Install : ConfiguredCmd
  
InstallApp : ConfiguredCmd
  
Remove : ConfiguredCmd
  
RemoveApp : ConfiguredCmd
  
Run : ConfiguredCmd
  
Test : ConfiguredCmd
  
New : ConfiguredCmd
  
Update : ConfiguredCmd
  
Fetch : ConfiguredCmd
  
PackagePath : ConfiguredCmd
  
LibsPath : ConfiguredCmd
  
DataPath : ConfiguredCmd
  
AppPath : ConfiguredCmd
  
Switch : ConfiguredCmd
  
UpdateDB : ConfiguredCmd
  
CollectGarbage : ConfiguredCmd
  
Info : ConfiguredCmd
  
Query : ConfiguredCmd
  
Fuzzy : ConfiguredCmd
  
Completion : ConfiguredCmd
  
Uninstall : ConfiguredCmd
  
PrintHelp : ConfiguredCmd

  Hint: 
Arg ConfiguredCmd
data Cmd : Type
  Commands accepted by *pack*. Most of these
  operate on a list of packages and/or
  projects with an `.ipkg` file.

  Totality: total
  Visibility: public export
  Constructors:
  
Trivial : TrivialCmd -> Cmd
  
Configured : ConfiguredCmd -> Cmd

  Hint: 
Arg Cmd
name : Cmd -> String
  Name to use at the command-line for running a pack command

  Totality: total
  Visibility: public export
commands : List ConfiguredCmd
  List of all available configured commands.
  
  `Pack.CmdLn.Types.cmdInCommands` proves that none were forgotten.

  Totality: total
  Visibility: public export
name : ConfiguredCmd -> String
  Name to use at the command-line for running a pack command

  Totality: total
  Visibility: public export
namesAndCommands : List (String, ConfiguredCmd)
  List pairing a command with its name used for parsing commands.

  Totality: total
  Visibility: public export
cmdDesc : ConfiguredCmd -> String
  Usage info for each configured command. This is printed when invoking `pack help <cmd>`.

  Totality: total
  Visibility: export
commands : List TrivialCmd
  List of all available trivial commands.
  
  `Pack.CmdLn.Types.cmdInCommands` proves that none were forgotten.

  Totality: total
  Visibility: public export
name : TrivialCmd -> String
  Name to use at the command-line for running a pack command

  Totality: total
  Visibility: public export
namesAndCommands : List (String, TrivialCmd)
  List pairing a command with its name used for parsing commands.

  Totality: total
  Visibility: public export
cmdDesc : TrivialCmd -> String
  Usage info for each trivial command. This is printed when invoking `pack help <cmd>`.

  Totality: total
  Visibility: export
namesAndCommands : List (String, Cmd)
  List pairing a command with its name used for parsing commands.

  Totality: total
  Visibility: public export