Matches the lengths of lists a
and b
by filling the shorter one with
unit
elements at the tail end. The matched lists are returned in the same order
as they were passed.
Equations
- Cli.List.matchLength a b unit = if a.length < b.length then (a ++ List.replicate (b.length - a.length) unit, b) else (a, b ++ List.replicate (a.length - b.length) unit)
Instances For
Equations
- Cli.Array.flatMap f xs = Cli.Array.join (Array.map f xs)
Instances For
Inserts newlines \n
into s
after every maxWidth
characters so that the result
contains no line longer than maxWidth
characters. Retains newlines \n
in s
.
Panics if maxWidth = 0
.
Equations
- Cli.String.wrapAt! s maxWidth = (Cli.String.wrapAt? s maxWidth).get!
Instances For
Deletes all trailing spaces at the end of every line, as seperated by \n
.
Equations
Instances For
Inserts newlines \n
into s
after every maxWidth
characters before words
that would otherwise be broken apart by the newline. The result will contain
no line longer than maxWidth
characters and no words except those already
longer than maxWidth
characters will be broken up in the middle.
Removes trailing whitespace before each inserted newline. Retains newlines \n
in s
.
Returns none
if maxWidth = 0
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Inserts newlines \n
into s
after every maxWidth
characters before words
that would otherwise be broken apart by the newline. The result will contain
no line longer than maxWidth
characters and no words except those already
longer than maxWidth
characters will be broken up in the middle.
Removes trailing whitespace before each inserted newline. Retains newlines \n
in s
.
Panics if maxWidth = 0
.
Equations
- Cli.String.wrapWordsAt! s maxWidth = (Cli.String.wrapWordsAt? s maxWidth).get!
Instances For
Intercalates elements ≠ ""
in xs
using sep
.
Equations
- Cli.String.optJoin xs sep = sep.intercalate (Array.filter (fun (x : String) => decide (x ≠ "")) xs).toList
Instances For
Renders rows
as a table with a maximum row width of maxWidth
and a margin of margin
between the columns. Wraps words according to String.wrapWordsAt?
to ensure that no
rendered row of the table is longer than maxWidth
.
Returns none
if (maxWidth-margin)/2
< 1, i.e. if there is not enough space for
text in both columns.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Renders rows
as a table with a maximum row width of maxWidth
and a margin of margin
between the columns. Wraps words according to String.wrapWordsAt?
to ensure that no
rendered row of the table is longer than maxWidth
.
Panics if (maxWidth-margin)/2
< 1, i.e. if there is not enough space for
text in both columns.
Equations
- Cli.Array.renderTable! rows maxWidth margin = (Cli.Array.renderTable? rows maxWidth margin).get!
Instances For
Equations
- Cli.Option.join x = do let __do_lift ← x __do_lift
Instances For
Returns ""
if the passed Option
is none
, otherwise
converts the contained value using a ToString
instance.
Equations
- Cli.Option.optStr none = ""
- Cli.Option.optStr (some v) = toString v
Instances For
Represents a type that can be parsed to a string and the corresponding name of the type. Used for converting parsed user input to the respective expected type.
- name : String
Name of the type, used when displaying the help.
Function to parse a value to the type that returns
none
if it cannot be parsed.
Instances
Equations
- Cli.instParseableTypeUnit = { name := "Unit", parse? := fun (x : String) => some () }
Equations
- Cli.instParseableTypeString = { name := "String", parse? := fun (s : String) => some s }
Equations
- Cli.instParseableTypeNat = { name := "Nat", parse? := fun (x : String) => match x with | "" => none | s => s.toNat? }
Equations
- Cli.instParseableTypeInt = { name := "Int", parse? := fun (x : String) => match x with | "" => none | s => s.toInt? }
A type synonym for Name
, which will carry a ParseableType ModuleName
instance, supporting parsing either a module name (e.g. Mathlib.Topology.Basic
)
or a relative path to a Lean file (e.g. Mathlib/Topology/Basic.lean
).
Equations
Instances For
Check that a ModuleName
has no .num
or empty components, and is not .anonymous
.
Equations
Instances For
Equations
- Cli.ModuleName.isValid.loop Lean.Name.anonymous x = x
- Cli.ModuleName.isValid.loop (pre.str s) x = Cli.ModuleName.isValid.loop pre (decide (x = true ∧ ¬s.isEmpty = true))
- Cli.ModuleName.isValid.loop (pre.num i) x = false
Instances For
A custom command-line argument parser that allows either relative paths to Lean files,
(e.g. Mathlib/Topology/Basic.lean
) or the module name (e.g. Mathlib.Topology.Basic
).
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Represents the type of some flag or argument parameter. Typically coerced from types with
ParseableType
instances such that isValid := (ParseableType.parse? · |>.isSome)
.
- name : String
Name of the type, used when displaying the help.
Function to check whether a value conforms to the type.
Instances For
Equations
- Cli.instInhabitedParamType = { default := { name := default, isValid := default } }
Equations
- Cli.instBEqParamType = { beq := fun (a b : Cli.ParamType) => a.name == b.name }
Equations
- Cli.instReprParamType = { reprPrec := fun (p : Cli.ParamType) (x : Nat) => Std.Format.text p.name }
Equations
- Cli.instCoeDepTypeParamTypeOfParseableType = { coe := { name := Cli.ParseableType.name τ, isValid := fun (x : String) => (Cli.ParseableType.parse? x).isSome } }
Represents a flag, usually known as "option" in standard terminology.
Designates
x
in-x
.- longName : String
Designates
x
in--x
. - description : String
Description that is displayed in the help.
- type : Cli.ParamType
Type according to which the parameter is validated.
Unit
is used to designate flags without a parameter.
Instances For
Equations
- Cli.instInhabitedFlag = { default := { shortName? := default, longName := default, description := default, type := default } }
Equations
- Cli.instReprFlag = { reprPrec := Cli.reprFlag✝ }
Initializes a flag without a parameter. Parameterless flags are
designated by the Unit
type.
shortName?
: Designatesx
in-x
.longName
: Designatesx
in--x
.description
: Description that is displayed in the help.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Checks whether f
has an associated short flag name x
in -x
.
Equations
- f.hasShortName = f.shortName?.isSome
Instances For
Checks whether f
has a Unit
type.
Equations
- f.isParamless = (f.type == { name := Cli.ParseableType.name Unit, isValid := fun (x : String) => (Cli.ParseableType.parse? x).isSome })
Instances For
Equations
- Cli.instInhabitedArg = { default := { name := default, description := default, type := default } }
Represents a flag and its parsed value.
Use Parsed.Flag.as!
to convert the value to some ParseableType
.
- flag : Cli.Flag
Associated flag meta-data.
- value : String
Parsed value that was validated and conforms to
flag.type
.
Instances For
Equations
- Cli.Parsed.instInhabitedFlag = { default := { flag := default, value := default } }
Equations
- Cli.Parsed.instBEqFlag = { beq := Cli.Parsed.beqFlag✝ }
Equations
- Cli.Parsed.instReprFlag = { reprPrec := Cli.Parsed.reprFlag✝ }
Equations
- One or more equations did not get rendered due to their size.
Converts f.value
to τ
, which should be the same type
that was designated in f.flag.type
.
Yields none
if the conversion was unsuccessful, which can only
happen if τ
is not the same type as the one designated in f.flag.type
.
Equations
- f.as? τ = Cli.ParseableType.parse? f.value
Instances For
Represents an argument and its parsed value.
Use Parsed.Arg.as!
to convert the value to some ParseableType
.
- arg : Cli.Arg
Associated argument meta-data.
- value : String
Parsed value that was validated and conforms to
arg.type
.
Instances For
Equations
- Cli.Parsed.instInhabitedArg = { default := { arg := default, value := default } }
Equations
- Cli.Parsed.instBEqArg = { beq := Cli.Parsed.beqArg✝ }
Equations
- Cli.Parsed.instReprArg = { reprPrec := Cli.Parsed.reprArg✝ }
Converts a.value
to τ
, which should be the same type
that was designated in a.arg.type
.
Yields none
if the conversion was unsuccessful, which can only
happen if τ
is not the same type as the one designated in a.arg.type
.
Equations
- a.as? τ = Cli.ParseableType.parse? a.value
Instances For
Represents all the non-recursive meta-data of a command.
- name : String
Name that is displayed in the help.
Names of the commands of which this command is a subcommand. Corresponds to the path from the root to this command.
Version of the command that is displayed in the help and when the version is queried.
- description : String
Description that is displayed in the help.
Information appended to the end of the help. Useful for command extensions.
Supported flags ("options" in standard terminology).
Supported positional arguments ("operands" in standard terminology).
Variable argument after the end of the positional arguments.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Cli.Cmd.instBEqMeta = { beq := Cli.Cmd.beqMeta✝ }
Equations
- Cli.Cmd.instReprMeta = { reprPrec := Cli.Cmd.reprMeta✝ }
Full name from the root to this command, including the name of the command itself.
Equations
- m.fullName = " ".intercalate (m.parentNames.push m.name).toList
Instances For
Version of the command that is displayed in the help and when the version is queried.
Equations
- m.version! = m.version?.get!
Instances For
Information appended to the end of the help. Useful for command extensions.
Equations
- m.furtherInformation! = m.furtherInformation?.get!
Instances For
Variable argument after the end of the positional arguments.
Equations
- m.variableArg! = m.variableArg?.get!
Instances For
Checks whether m
has information appended to the end of the help.
Equations
- m.hasFurtherInformation = m.furtherInformation?.isSome
Instances For
Checks whether m
supports a variable argument.
Equations
- m.hasVariableArg = m.variableArg?.isSome
Instances For
Finds the flag in m
with the corresponding shortName
.
Equations
Instances For
Finds the flag in m
with the corresponding shortName
.
Equations
- m.flagByShortName! name = (m.flagByShortName? name).get!
Instances For
Checks whether m
has a flag with the corresponding shortName
.
Equations
- m.hasFlagByShortName name = (m.flagByShortName? name).isSome
Instances For
Adds help (-h, --help
) and version (--version
) flags to m
. Does not add
a version flag if m
does not designate a version.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Represents a recursive variant of Cmd.Meta
that is used in Parsed
to replicate the recursive subcommand structure of a command
without referring to the command itself.
- init: Cli.Cmd.Meta → Array Cli.Parsed.Cmd → Cli.Parsed.Cmd
Instances For
Equations
- Cli.Parsed.instInhabitedCmd = { default := Cli.Parsed.Cmd.init default default }
Finds the subcommand in c
with the corresponding name
.
Equations
- c.subCmd? name = c.subCmds.find? fun (x : Cli.Parsed.Cmd) => decide (x.meta.name = name)
Instances For
Represents parsed user input data.
- cmd : Cli.Parsed.Cmd
Recursive meta-data of the associated command.
- parent? : Option Cli.Parsed.Cmd
Parent of the associated command.
- flags : Array Cli.Parsed.Flag
Parsed flags.
- positionalArgs : Array Cli.Parsed.Arg
Parsed positional arguments.
- variableArgs : Array Cli.Parsed.Arg
Parsed variable arguments.
Instances For
Equations
- Cli.instInhabitedParsed = { default := { cmd := default, parent? := default, flags := default, positionalArgs := default, variableArgs := default } }
Checks whether the associated command has a parent, i.e. whether it is not the root command.
Equations
- p.hasParent = p.parent?.isSome
Instances For
Finds the parsed flag in p
with the corresponding longName
.
Equations
- p.flag? longName = p.flags.find? fun (x : Cli.Parsed.Flag) => decide (x.flag.longName = longName)
Instances For
Finds the parsed positional argument in p
with the corresponding name
.
Equations
- p.positionalArg? name = p.positionalArgs.find? fun (x : Cli.Parsed.Arg) => decide (x.arg.name = name)
Instances For
Converts all p.variableArgs
values to τ
, which should be the same type
that was designated in the corresponding Cli.Arg
.
Yields none
if the conversion was unsuccessful, which can only
happen if τ
is not the same type as the one designated in the corresponding Cli.Arg
.
Equations
- p.variableArgsAs? τ = Array.mapM (fun (x : Cli.Parsed.Arg) => x.as? τ) p.variableArgs
Instances For
Converts all p.variableArgs
values to τ
, which should be the same type
that was designated in the corresponding Cli.Arg
.
Panics if the conversion was unsuccessful, which can only
happen if τ
is not the same type as the one designated in the corresponding Cli.Arg
.
Equations
- p.variableArgsAs! τ = (p.variableArgsAs? τ).get!
Instances For
Equations
- One or more equations did not get rendered due to their size.
Represents a view of Cmd
that can be passed to Extension
s, i.e. it does
not itself reference the Extension
provided for each Cmd
.
- init: Cli.Cmd.Meta → (Cli.Parsed → IO UInt32) → Array Cli.ExtendableCmd → Option String → Cli.ExtendableCmd
Instances For
Equations
- Cli.instInhabitedExtendableCmd = { default := Cli.ExtendableCmd.init default default default default }
Non-recursive meta-data.
Equations
- (Cli.ExtendableCmd.init v run subCmds originalFullName?).meta = v
Instances For
Handler to run when the command is called and flags/arguments have been successfully processed.
Equations
- (Cli.ExtendableCmd.init v run subCmds originalFullName?).run = run
Instances For
Subcommands. May be mutated by extensions.
Equations
- (Cli.ExtendableCmd.init v run subCmds originalFullName?).subCmds = subCmds
Instances For
Updates the designated fields in c
.
meta
: Non-recursive meta-data.run
: Handler to run when the command is called and flags/arguments have been successfully processed.subCmds
: Subcommands.
Equations
- c.update' meta run subCmds = Cli.ExtendableCmd.init meta run subCmds (Cli.ExtendableCmd.originalFullName? c)
Instances For
Updates the designated fields in c
.
name
: Name that is displayed in the help.version?
: Version that is displayed in the help and when the version is queried.description
: Description that is displayed in the help.furtherInformation?
: Information appended to the end of the help. Useful for command extensions.flags
: Supported flags ("options" in standard terminology).positionalArgs
: Supported positional arguments ("operands" in standard terminology).variableArg?
: Variable argument at the end of the positional arguments.run
: Handler to run when the command is called and flags/arguments have been successfully processed.subCmds
: Subcommands.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Creates a new ExtendableCmd
. The resulting ExtendableCmd
will not have an extension.
meta
: Non-recursive meta-data.run
: Handler to run when the command is called and flags/arguments have been successfully processed.subCmds
: Subcommands.
Equations
- Cli.ExtendableCmd.mk' meta run subCmds = Cli.ExtendableCmd.init meta run subCmds none
Instances For
Creates a new ExtendableCmd
. The resulting ExtendableCmd
will not have an extension.
Adds a -h, --help
and a --version
flag if meta
designates a version.
meta
: Non-recursive meta-data.run
: Handler to run when the command is called and flags/arguments have been successfully processed.subCmds
: Subcommands.
Equations
- Cli.ExtendableCmd.mkWithHelpAndVersionFlags' meta run subCmds = Cli.ExtendableCmd.mk' meta.addHelpAndVersionFlags run subCmds
Instances For
Creates a new ExtendableCmd
. The resulting ExtendableCmd
will not have an extension.
parent
: Parent of this command.name
: Name that is displayed in the help.version?
: Version that is displayed in the help and when the version is queried.description
: Description that is displayed in the help.furtherInformation?
: Information appended to the end of the help. Useful for command extensions.flags
: Supported flags ("options" in standard terminology).positionalArgs
: Supported positional arguments ("operands" in standard terminology).variableArg?
: Variable argument at the end of the positional arguments.run
: Handler to run when the command is called and flags/arguments have been successfully processed.subCmds
: Subcommands.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Creates a new ExtendableCmd
. The resulting ExtendableCmd
will not have an extension.
Adds a -h, --help
and a --version
flag if version?
is present.
parent
: Parent of this command.name
: Name that is displayed in the help.version?
: Version that is displayed in the help and when the version is queried.description
: Description that is displayed in the help.furtherInformation?
: Information appended to the end of the help. Useful for command extensions.flags
: Supported flags ("options" in standard terminology).positionalArgs
: Supported positional arguments ("operands" in standard terminology).variableArg?
: Variable argument at the end of the positional arguments.run
: Handler to run when the command is called and flags/arguments have been successfully processed.subCmds
: Subcommands.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Version of the command that is displayed in the help and when the version is queried.
Equations
- c.version? = c.meta.version?
Instances For
Information appended to the end of the help. Useful for command extensions.
Equations
- c.furtherInformation? = c.meta.furtherInformation?
Instances For
Supported positional arguments ("operands" in standard terminology).
Equations
- c.positionalArgs = c.meta.positionalArgs
Instances For
Variable argument after the end of the positional arguments.
Equations
- c.variableArg? = c.meta.variableArg?
Instances For
Full name from the root to this command, including the name of the command itself.
Equations
- c.fullName = c.meta.fullName
Instances For
Version of the command that is displayed in the help and when the version is queried.
Equations
- c.version! = c.meta.version!
Instances For
Information appended to the end of the help. Useful for command extensions.
Equations
- c.furtherInformation! = c.meta.furtherInformation!
Instances For
Variable argument after the end of the positional arguments.
Equations
- c.variableArg! = c.meta.variableArg!
Instances For
Checks whether c
has information appended to the end of the help.
Equations
- c.hasFurtherInformation = c.meta.hasFurtherInformation
Instances For
Checks whether c
supports a variable argument.
Equations
- c.hasVariableArg = c.meta.hasVariableArg
Instances For
Finds the flag in c
with the corresponding shortName
.
Equations
- c.flagByShortName? name = c.meta.flagByShortName? name
Instances For
Finds the subcommand in c
with the corresponding name
.
Equations
- c.subCmd? name = c.subCmds.find? fun (x : Cli.ExtendableCmd) => decide (x.meta.name = name)
Instances For
Finds the flag in c
with the corresponding shortName
.
Equations
- c.flagByShortName! name = c.meta.flagByShortName! name
Instances For
Checks whether c
has a flag with the corresponding shortName
.
Equations
- c.hasFlagByShortName name = c.meta.hasFlagByShortName name
Instances For
Allows user code to extend the library in two ways:
- A command can be replaced or extended with new components.
- The output of the parser can be postprocessed and validated.
- priority : Nat
Priority that dictates how early an extension is applied. The lower the priority, the later it is applied.
- extend : Cli.ExtendableCmd → Cli.ExtendableCmd
Extends a command to adjust the displayed help. The recursive subcommand structure may be mutated.
- postprocess : Cli.ExtendableCmd → Cli.Parsed → Except String Cli.Parsed
Processes and validates the output of the parser for the given
ExtendableCmd
. Takes theExtendableCmd
that results from all extensions being applied. If postprocessing mutates the subcommand structure inParsed.cmd
, care must be taken to updateParsed.parent?
accordingly as well.
Instances For
Equations
- Cli.instInhabitedExtension = { default := { priority := default, extend := default, postprocess := default } }
Composes both extensions so that the Cmd
s are extended in succession
and postprocessed in succession. Postprocessing errors if any of the two
postprocess
functions errors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Represents a command, i.e. either the application root or some subcommand of the root.
- init: Cli.Cmd.Meta → (Cli.Parsed → IO UInt32) → Array Cli.Cmd → Option Cli.Extension → Cli.Cmd
Instances For
Equations
- Cli.instInhabitedCmd = { default := Cli.Cmd.init default default default default }
Handler to run when the command is called and flags/arguments have been successfully processed.
Equations
- (Cli.Cmd.init v run subCmds extension?).run = run
Instances For
Extension of the Cli library.
Equations
- (Cli.Cmd.init v run subCmds extension?).extension? = extension?
Instances For
Recomputes all the parent names of subcommands in c
with c
as the root command.
Equations
- c.updateParentNames = Cli.Cmd.updateParentNames.loop c #[]
Instances For
Creates a new command. Adds a -h, --help
and a --version
flag if meta
designates a version.
Updates the parentNames
of all subcommands.
meta
: Non-recursive meta-data.run
: Handler to run when the command is called and flags/arguments have been successfully processed.subCmds
: Subcommands.extension?
: Extension of the Cli library.
Equations
- Cli.Cmd.mk' meta run subCmds extension? = (Cli.Cmd.init meta.addHelpAndVersionFlags run subCmds extension?).updateParentNames
Instances For
Creates a new command. Adds a -h, --help
and a --version
flag if a version is designated.
Updates the parentNames
of all subcommands.
name
: Name that is displayed in the help.version?
: Version that is displayed in the help and when the version is queried.description
: Description that is displayed in the help.furtherInformation?
: Information appended to the end of the help. Useful for command extensions.flags
: Supported flags ("options" in standard terminology).positionalArgs
: Supported positional arguments ("operands" in standard terminology).variableArg?
: Variable argument at the end of the positional arguments.run
: Handler to run when the command is called and flags/arguments have been successfully processed.subCmds
: Subcommands.extension?
: Extension of the Cli library.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extracts meta
and the recursive subcommand structure from c
to create a Parsed.Cmd
.
Embeds c
into a Cli.Cmd
that does nothing.
Creates a view of c
that can be extended by extensions.
Converts c
back into a Cli.Cmd
, using the extensions denoted in original
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Converts c
back into Cli.Cmd
while retaining none of the extensions.
Equations
- Cli.literalIdent = Lean.ParserDescr.nodeWithAntiquot "literalIdent" `Cli.literalIdent (Lean.ParserDescr.cat `term 0)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Amount of spaces with which section content is indented.
Equations
Instances For
Maximum width within which all formatted text should fit, after indentation.
Equations
Instances For
Formats xs
by String.optJoin
ing the components with a single space.
Equations
- Cli.line xs = Cli.String.optJoin xs " "
Instances For
Formats xs
by String.optJoin
ing the components with a newline \n
.
Equations
- Cli.lines xs = Cli.String.optJoin xs "\n"
Instances For
Renders a help section with the designated title
and content
.
If content = ""
, emptyContentPlaceholder?
will be used instead.
If emptyContentPlaceholder? = none
, neither the title nor the content
will be rendered.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Renders a table using Cli.Array.renderTable!
and then renders a section with
the designated title
and the rendered table as content.
Equations
- Cli.renderTable title columns emptyTablePlaceholder? = Cli.renderSection title (Cli.Array.renderTable! columns Cli.maxIndentedWidth) emptyTablePlaceholder?
Instances For
Renders the help for c
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prints an error for c
with the designated message msg
.
Equations
- c.printError msg = IO.eprintln (c.error msg)
Instances For
Prints the version of c
. Panics if c
has no version.
Equations
- c.printVersion! = IO.println c.meta.version!
Instances For
Equations
- One or more equations did not get rendered due to their size.
Represents the kind of error that occured during parsing.
- unknownFlag: (inputFlag : Cli.InputFlag) → optParam String (toString "Unknown flag `" ++ toString inputFlag ++ toString "`.") → Cli.ParseError.Kind
- missingFlagArg: Cli.Flag → (inputFlag : Cli.InputFlag) → optParam String (toString "Missing argument for flag `" ++ toString inputFlag ++ toString "`.") → Cli.ParseError.Kind
- duplicateFlag: (flag : Cli.Flag) → (inputFlag : Cli.InputFlag) → optParam String (let complementaryName? := if inputFlag.isShort = true then pure (toString " (`--" ++ toString flag.longName ++ toString "`)") else do let __do_lift ← flag.shortName? pure (toString " (`-" ++ toString __do_lift ++ toString "`)"); toString "Duplicate flag `" ++ toString inputFlag ++ toString "`" ++ toString (Cli.Option.optStr complementaryName?) ++ toString ".") → Cli.ParseError.Kind
- redundantFlagArg: Cli.Flag → (inputFlag : Cli.InputFlag) → (inputValue : String) → optParam String (toString "Redundant argument `" ++ toString inputValue ++ toString "` for flag `" ++ toString inputFlag ++ toString "` that takes no arguments.") → Cli.ParseError.Kind
- invalidFlagType: (flag : Cli.Flag) → (inputFlag : Cli.InputFlag) → (inputValue : String) → optParam String (toString "Invalid type of argument `" ++ toString inputValue ++ toString "` for flag `" ++ toString inputFlag ++ toString " : " ++ toString flag.type.name ++ toString "`.") → Cli.ParseError.Kind
- missingPositionalArg: (arg : Cli.Arg) → optParam String (toString "Missing positional argument `<" ++ toString arg.name ++ toString ">.`") → Cli.ParseError.Kind
- invalidPositionalArgType: (arg : Cli.Arg) → (inputArg : String) → optParam String (toString "Invalid type of argument `" ++ toString inputArg ++ toString "` for positional argument `<" ++ toString arg.name ++ toString " : " ++ toString arg.type.name ++ toString ">`.") → Cli.ParseError.Kind
- redundantPositionalArg: (inputArg : String) → optParam String (toString "Redundant positional argument `" ++ toString inputArg ++ toString "`.") → Cli.ParseError.Kind
- invalidVariableArgType: (arg : Cli.Arg) → (inputArg : String) → optParam String (toString "Invalid type of argument `" ++ toString inputArg ++ toString "` for variable argument `<" ++ toString arg.name ++ toString " : " ++ toString arg.type.name ++ toString ">...`.") → Cli.ParseError.Kind
Instances For
Associated message of the error.
Equations
- (Cli.ParseError.Kind.unknownFlag inputFlag msg).msg = msg
- (Cli.ParseError.Kind.missingFlagArg flag inputFlag msg).msg = msg
- (Cli.ParseError.Kind.duplicateFlag flag inputFlag msg).msg = msg
- (Cli.ParseError.Kind.redundantFlagArg flag inputFlag inputValue msg).msg = msg
- (Cli.ParseError.Kind.invalidFlagType flag inputFlag inputValue msg).msg = msg
- (Cli.ParseError.Kind.missingPositionalArg arg msg).msg = msg
- (Cli.ParseError.Kind.invalidPositionalArgType arg inputArg msg).msg = msg
- (Cli.ParseError.Kind.redundantPositionalArg inputArg msg).msg = msg
- (Cli.ParseError.Kind.invalidVariableArgType arg inputArg msg).msg = msg
Instances For
Error that occured during parsing. Contains the command that the error occured in and the kind of the error.
- cmd : Cli.Cmd
Command that the error occured in.
- kind : Cli.ParseError.Kind
Kind of error that occured.
Instances For
Parses args
according to the specification provided in c
, returning either a ParseError
or the
(sub)command that was called and the parsed content of the input.
Note that args
designates the list <foo>
in somebinary <foo>
.
Equations
- c.parse args = Cli.ParseM.parse c args
Instances For
Recursively applies extensions in all subcommands in c
bottom-up and c
itself.
Processes args
by applying all extensions in c
, Cmd.parse?
ing the input according to c
and then applying the postprocessing extension of the respective (sub)command that was called.
Note that args
designates the list <foo>
in somebinary <foo>
.
Returns either the (sub)command that an error occured in and the corresponding error message or
the (sub)command that was called and the parsed input after postprocessing.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Validates args
by Cmd.process?
ing the input according to c
.
Note that args
designates the list <foo>
in somebinary <foo>
.
Prints the help or the version of the called (sub)command if the respective flag was passed and
returns 0
for the exit code.
If neither of these flags were passed and processing was successful, the run
handler of the
called command is executed.
In the case of a processing error, the error is printed to stderr and an exit code of 1
is returned.
Equations
- One or more equations did not get rendered due to their size.