def Cli.List.matchLength {α : Type u_1} (a : List α) (b : List α) (unit : α) : List α × List α

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)

def Cli.Array.join {α : Type u_1} (xss : Array (Array α)) : Array α

Equations

• One or more equations did not get rendered due to their size.

def Cli.Array.flatMap {α : Type u_1} {β : Type u_2} (f : α → Array β) (xs : Array α) : Array β

Equations

• Cli.Array.flatMap f xs = Cli.Array.join (Array.map f xs)

def Cli.String.wrapAt? (s : String) (maxWidth : Nat) : Option String

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. Yields none if maxWidth = 0.

Equations

• One or more equations did not get rendered due to their size.

def Cli.String.wrapAt! (s : String) (maxWidth : Nat) : String

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!

def Cli.String.trimTrailingSpaces (s : String) : String

Deletes all trailing spaces at the end of every line, as seperated by \n.

Equations

• Cli.String.trimTrailingSpaces s = "\n".intercalate (List.map (fun (x : String) => x.dropRightWhile fun (x : Char) => decide (x = ' ')) (s.splitOn "\n"))

def Cli.String.wrapWordsAt? (s : String) (maxWidth : Nat) : Option String

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.

def Cli.String.wrapWordsAt! (s : String) (maxWidth : Nat) : String

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!

def Cli.String.indent (s : String) (n : optParam Nat 4) : String

Inserts n spaces before each line as seperated by \n in s. Does not indent s = "".

Equations

• One or more equations did not get rendered due to their size.

def Cli.String.optJoin (xs : Array String) (sep : String) : String

Intercalates elements ≠ "" in xs using sep.

Equations

• Cli.String.optJoin xs sep = sep.intercalate (Array.filter (fun (x : String) => decide (x ≠ "")) xs).toList

def Cli.Array.renderTable? (rows : Array (String × String)) (maxWidth : Nat) (margin : optParam Nat 2) : Option String

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.

def Cli.Array.renderTable! (rows : Array (String × String)) (maxWidth : Nat) (margin : optParam Nat 2) : String

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!

def Cli.Option.join {α : Type u_1} (x : Option (Option α)) : Option α

Equations

• Cli.Option.join x = do let __do_lift ← x __do_lift

def Cli.Option.optStr {α : Type u_1} [ToString α] : Option α → String

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

class Cli.ParseableType (τ : Type u_1) : Type u_1

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.

• parse? : String → Option τ

  Function to parse a value to the type that returns none if it cannot be parsed.

instance Cli.instParseableTypeUnit : Cli.ParseableType Unit

Equations

• Cli.instParseableTypeUnit = { name := "Unit", parse? := fun (x : String) => some () }

instance Cli.instParseableTypeBool : Cli.ParseableType Bool

Equations

• Cli.instParseableTypeBool = { name := "Bool", parse? := fun (x : String) => match x with | "true" => some true | "false" => some false | x => none }

instance Cli.instParseableTypeString : Cli.ParseableType String

Equations

• Cli.instParseableTypeString = { name := "String", parse? := fun (s : String) => some s }

instance Cli.instParseableTypeNat : Cli.ParseableType Nat

Equations

• Cli.instParseableTypeNat = { name := "Nat", parse? := fun (x : String) => match x with | "" => none | s => s.toNat? }

instance Cli.instParseableTypeInt : Cli.ParseableType Int

Equations

• Cli.instParseableTypeInt = { name := "Int", parse? := fun (x : String) => match x with | "" => none | s => s.toInt? }

def Cli.ModuleName : Type

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

• Cli.ModuleName = Lean.Name

def Cli.ModuleName.isValid : Cli.ModuleName → Bool

Check that a ModuleName has no .num or empty components, and is not .anonymous.

Equations

• Cli.ModuleName.isValid Lean.Name.anonymous = false
• x.isValid = Cli.ModuleName.isValid.loop x true

def Cli.ModuleName.isValid.loop : Cli.ModuleName → Bool → Bool

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

instance Cli.instParseableTypeModuleName : Cli.ParseableType Cli.ModuleName

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.

instance Cli.instParseableTypeArray {α : Type u_1} [inst : Cli.ParseableType α] : Cli.ParseableType (Array α)

Equations

• One or more equations did not get rendered due to their size.

structure Cli.ParamType : Type

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.

• isValid : String → Bool

  Function to check whether a value conforms to the type.

instance Cli.instInhabitedParamType : Inhabited Cli.ParamType

Equations

• Cli.instInhabitedParamType = { default := { name := default, isValid := default } }

instance Cli.instBEqParamType : BEq Cli.ParamType

Equations

• Cli.instBEqParamType = { beq := fun (a b : Cli.ParamType) => a.name == b.name }

instance Cli.instReprParamType : Repr Cli.ParamType

Equations

• Cli.instReprParamType = { reprPrec := fun (p : Cli.ParamType) (x : Nat) => Std.Format.text p.name }

instance Cli.instCoeDepTypeParamTypeOfParseableType {τ : Type} [inst : Cli.ParseableType τ] : CoeDep Type τ Cli.ParamType

Equations

• Cli.instCoeDepTypeParamTypeOfParseableType = { coe := { name := Cli.ParseableType.name τ, isValid := fun (x : String) => (Cli.ParseableType.parse? x).isSome } }

structure Cli.Flag : Type

Represents a flag, usually known as "option" in standard terminology.

• shortName? : Option String

  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.

instance Cli.instInhabitedFlag : Inhabited Cli.Flag

Equations

• Cli.instInhabitedFlag = { default := { shortName? := default, longName := default, description := default, type := default } }

instance Cli.instBEqFlag : BEq Cli.Flag

Equations

• Cli.instBEqFlag = { beq := Cli.beqFlag✝ }

instance Cli.instReprFlag : Repr Cli.Flag

Equations

• Cli.instReprFlag = { reprPrec := Cli.reprFlag✝ }

def Cli.Flag.paramless (shortName? : optParam (Option String) none) (longName : String) (description : String) : Cli.Flag

Initializes a flag without a parameter. Parameterless flags are designated by the Unit type.

• shortName?: Designates x in -x.
• longName: Designates x in --x.
• description: Description that is displayed in the help.

Equations

• One or more equations did not get rendered due to their size.

def Cli.Flag.shortName! (f : Cli.Flag) : String

Designates x in -x.

Equations

• f.shortName! = f.shortName?.get!

def Cli.Flag.hasShortName (f : Cli.Flag) : Bool

Checks whether f has an associated short flag name x in -x.

Equations

• f.hasShortName = f.shortName?.isSome

def Cli.Flag.isParamless (f : Cli.Flag) : Bool

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 })

structure Cli.Arg : Type

Represents an argument (either positional or variable), usually known as "operand" in standard terminology

• name : String
• description : String
• type : Cli.ParamType

instance Cli.instInhabitedArg : Inhabited Cli.Arg

Equations

• Cli.instInhabitedArg = { default := { name := default, description := default, type := default } }

instance Cli.instBEqArg : BEq Cli.Arg

Equations

• Cli.instBEqArg = { beq := Cli.beqArg✝ }

instance Cli.instReprArg : Repr Cli.Arg

Equations

• Cli.instReprArg = { reprPrec := Cli.reprArg✝ }

structure Cli.Parsed.Flag : Type

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.

instance Cli.Parsed.instInhabitedFlag : Inhabited Cli.Parsed.Flag

Equations

• Cli.Parsed.instInhabitedFlag = { default := { flag := default, value := default } }

instance Cli.Parsed.instBEqFlag : BEq Cli.Parsed.Flag

Equations

• Cli.Parsed.instBEqFlag = { beq := Cli.Parsed.beqFlag✝ }

instance Cli.Parsed.instReprFlag : Repr Cli.Parsed.Flag

Equations

• Cli.Parsed.instReprFlag = { reprPrec := Cli.Parsed.reprFlag✝ }

instance Cli.Parsed.instToStringFlag : ToString Cli.Parsed.Flag

Equations

• One or more equations did not get rendered due to their size.

def Cli.Parsed.Flag.as? (f : Cli.Parsed.Flag) (τ : Type u_1) [Cli.ParseableType τ] : Option τ

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

def Cli.Parsed.Flag.as! (f : Cli.Parsed.Flag) (τ : Type u_1) [Inhabited τ] [Cli.ParseableType τ] : τ

Converts f.value to τ, which should be the same type that was designated in f.flag.type. Panics 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! τ = (f.as? τ).get!

structure Cli.Parsed.Arg : Type

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.

instance Cli.Parsed.instInhabitedArg : Inhabited Cli.Parsed.Arg

Equations

• Cli.Parsed.instInhabitedArg = { default := { arg := default, value := default } }

instance Cli.Parsed.instBEqArg : BEq Cli.Parsed.Arg

Equations

• Cli.Parsed.instBEqArg = { beq := Cli.Parsed.beqArg✝ }

instance Cli.Parsed.instReprArg : Repr Cli.Parsed.Arg

Equations

• Cli.Parsed.instReprArg = { reprPrec := Cli.Parsed.reprArg✝ }

instance Cli.Parsed.instToStringArg : ToString Cli.Parsed.Arg

Equations

• Cli.Parsed.instToStringArg = { toString := fun (a : Cli.Parsed.Arg) => toString "<" ++ toString a.arg.name ++ toString "=" ++ toString a.value ++ toString ">" }

def Cli.Parsed.Arg.as? (a : Cli.Parsed.Arg) (τ : Type u_1) [Cli.ParseableType τ] : Option τ

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

def Cli.Parsed.Arg.as! (a : Cli.Parsed.Arg) (τ : Type u_1) [Inhabited τ] [Cli.ParseableType τ] : τ

Converts a.value to τ, which should be the same type that was designated in a.arg.type. Panics 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! τ = (a.as? τ).get!

structure Cli.Cmd.Meta : Type

Represents all the non-recursive meta-data of a command.

• name : String

  Name that is displayed in the help.

• parentNames : Array String

  Names of the commands of which this command is a subcommand. Corresponds to the path from the root to this command.

• version? : Option String

  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.

• furtherInformation? : Option String

  Information appended to the end of the help. Useful for command extensions.

• flags : Array Cli.Flag

  Supported flags ("options" in standard terminology).

• positionalArgs : Array Cli.Arg

  Supported positional arguments ("operands" in standard terminology).

• variableArg? : Option Cli.Arg

  Variable argument after the end of the positional arguments.

instance Cli.Cmd.instInhabitedMeta : Inhabited Cli.Cmd.Meta

Equations

• One or more equations did not get rendered due to their size.

instance Cli.Cmd.instBEqMeta : BEq Cli.Cmd.Meta

Equations

• Cli.Cmd.instBEqMeta = { beq := Cli.Cmd.beqMeta✝ }

instance Cli.Cmd.instReprMeta : Repr Cli.Cmd.Meta

Equations

• Cli.Cmd.instReprMeta = { reprPrec := Cli.Cmd.reprMeta✝ }

def Cli.Cmd.Meta.fullName (m : Cli.Cmd.Meta) : String

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

def Cli.Cmd.Meta.version! (m : Cli.Cmd.Meta) : String

Version of the command that is displayed in the help and when the version is queried.

Equations

• m.version! = m.version?.get!

def Cli.Cmd.Meta.furtherInformation! (m : Cli.Cmd.Meta) : String

Information appended to the end of the help. Useful for command extensions.

Equations

• m.furtherInformation! = m.furtherInformation?.get!

def Cli.Cmd.Meta.variableArg! (m : Cli.Cmd.Meta) : Cli.Arg

Variable argument after the end of the positional arguments.

Equations

• m.variableArg! = m.variableArg?.get!

def Cli.Cmd.Meta.hasVersion (m : Cli.Cmd.Meta) : Bool

Checks whether m has a version.

Equations

• m.hasVersion = m.version?.isSome

def Cli.Cmd.Meta.hasFurtherInformation (m : Cli.Cmd.Meta) : Bool

Checks whether m has information appended to the end of the help.

Equations

• m.hasFurtherInformation = m.furtherInformation?.isSome

def Cli.Cmd.Meta.hasVariableArg (m : Cli.Cmd.Meta) : Bool

Checks whether m supports a variable argument.

Equations

• m.hasVariableArg = m.variableArg?.isSome

def Cli.Cmd.Meta.flag? (m : Cli.Cmd.Meta) (longName : String) : Option Cli.Flag

Finds the flag in m with the corresponding longName.

Equations

• m.flag? longName = m.flags.find? fun (x : Cli.Flag) => decide (x.longName = longName)

def Cli.Cmd.Meta.positionalArg? (m : Cli.Cmd.Meta) (name : String) : Option Cli.Arg

Finds the positional argument in m with the corresponding name.

Equations

• m.positionalArg? name = m.positionalArgs.find? fun (x : Cli.Arg) => decide (x.name = name)

def Cli.Cmd.Meta.flag! (m : Cli.Cmd.Meta) (longName : String) : Cli.Flag

Finds the flag in m with the corresponding longName.

Equations

• m.flag! longName = (m.flag? longName).get!

def Cli.Cmd.Meta.positionalArg! (m : Cli.Cmd.Meta) (name : String) : Cli.Arg

Finds the positional argument in m with the corresponding name.

Equations

• m.positionalArg! name = (m.positionalArg? name).get!

def Cli.Cmd.Meta.hasFlag (m : Cli.Cmd.Meta) (longName : String) : Bool

Checks whether m contains a flag with the corresponding longName.

Equations

• m.hasFlag longName = (m.flag? longName).isSome

def Cli.Cmd.Meta.hasPositionalArg (m : Cli.Cmd.Meta) (name : String) : Bool

Checks whether m contains a positional argument with the corresponding name.

Equations

• m.hasPositionalArg name = (m.positionalArg? name).isSome

def Cli.Cmd.Meta.flagByShortName? (m : Cli.Cmd.Meta) (name : String) : Option Cli.Flag

Finds the flag in m with the corresponding shortName.

Equations

• m.flagByShortName? name = m.flags.findSome? fun (flag : Cli.Flag) => do let shortName ← flag.shortName? guard (shortName = name) pure flag

def Cli.Cmd.Meta.flagByShortName! (m : Cli.Cmd.Meta) (name : String) : Cli.Flag

Finds the flag in m with the corresponding shortName.

Equations

• m.flagByShortName! name = (m.flagByShortName? name).get!

def Cli.Cmd.Meta.hasFlagByShortName (m : Cli.Cmd.Meta) (name : String) : Bool

Checks whether m has a flag with the corresponding shortName.

Equations

• m.hasFlagByShortName name = (m.flagByShortName? name).isSome

def Cli.Cmd.Meta.addHelpAndVersionFlags (m : Cli.Cmd.Meta) : Cli.Cmd.Meta

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.

inductive Cli.Parsed.Cmd : Type

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

instance Cli.Parsed.instInhabitedCmd : Inhabited Cli.Parsed.Cmd

Equations

• Cli.Parsed.instInhabitedCmd = { default := Cli.Parsed.Cmd.init default default }

def Cli.Parsed.Cmd.meta : Cli.Parsed.Cmd → Cli.Cmd.Meta

Meta of this command.

Equations

• (Cli.Parsed.Cmd.init v subCmds).meta = v

def Cli.Parsed.Cmd.subCmds : Cli.Parsed.Cmd → Array Cli.Parsed.Cmd

Subcommands.

Equations

• (Cli.Parsed.Cmd.init v subCmds).subCmds = subCmds

def Cli.Parsed.Cmd.subCmd? (c : Cli.Parsed.Cmd) (name : String) : Option Cli.Parsed.Cmd

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)

def Cli.Parsed.Cmd.subCmd! (c : Cli.Parsed.Cmd) (name : String) : Cli.Parsed.Cmd

Finds the subcommand in c with the corresponding name.

Equations

• c.subCmd! name = (c.subCmd? name).get!

def Cli.Parsed.Cmd.hasSubCmd (c : Cli.Parsed.Cmd) (name : String) : Bool

Checks whether c contains a subcommand with the corresponding name.

Equations

• c.hasSubCmd name = (c.subCmd? name).isSome

structure Cli.Parsed : Type

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.

instance Cli.instInhabitedParsed : Inhabited Cli.Parsed

Equations

• Cli.instInhabitedParsed = { default := { cmd := default, parent? := default, flags := default, positionalArgs := default, variableArgs := default } }

def Cli.Parsed.parent! (p : Cli.Parsed) : Cli.Parsed.Cmd

Parent of the associated command.

Equations

• p.parent! = p.parent?.get!

def Cli.Parsed.hasParent (p : Cli.Parsed) : Bool

Checks whether the associated command has a parent, i.e. whether it is not the root command.

Equations

• p.hasParent = p.parent?.isSome

def Cli.Parsed.flag? (p : Cli.Parsed) (longName : String) : Option Cli.Parsed.Flag

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)

def Cli.Parsed.positionalArg? (p : Cli.Parsed) (name : String) : Option Cli.Parsed.Arg

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)

def Cli.Parsed.flag! (p : Cli.Parsed) (longName : String) : Cli.Parsed.Flag

Finds the parsed flag in p with the corresponding longName.

Equations

• p.flag! longName = (p.flag? longName).get!

def Cli.Parsed.positionalArg! (p : Cli.Parsed) (name : String) : Cli.Parsed.Arg

Finds the parsed positional argument in p with the corresponding name.

Equations

• p.positionalArg! name = (p.positionalArg? name).get!

def Cli.Parsed.hasFlag (p : Cli.Parsed) (longName : String) : Bool

Checks whether p has a parsed flag with the corresponding longName.

Equations

• p.hasFlag longName = (p.flag? longName).isSome

def Cli.Parsed.hasPositionalArg (p : Cli.Parsed) (name : String) : Bool

Checks whether p has a positional argument with the corresponding longName.

Equations

• p.hasPositionalArg name = (p.positionalArg? name).isSome

def Cli.Parsed.variableArgsAs? (p : Cli.Parsed) (τ : Type u_1) [Cli.ParseableType τ] : Option (Array τ)

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

def Cli.Parsed.variableArgsAs! (p : Cli.Parsed) (τ : Type u_1) [Inhabited τ] [Cli.ParseableType τ] : Array τ

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!

instance Cli.Parsed.instToString : ToString Cli.Parsed

Equations

• One or more equations did not get rendered due to their size.

inductive Cli.ExtendableCmd : Type

Represents a view of Cmd that can be passed to Extensions, 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

instance Cli.instInhabitedExtendableCmd : Inhabited Cli.ExtendableCmd

Equations

• Cli.instInhabitedExtendableCmd = { default := Cli.ExtendableCmd.init default default default default }

def Cli.ExtendableCmd.meta : Cli.ExtendableCmd → Cli.Cmd.Meta

Non-recursive meta-data.

Equations

• (Cli.ExtendableCmd.init v run subCmds originalFullName?).meta = v

def Cli.ExtendableCmd.run : Cli.ExtendableCmd → Cli.Parsed → IO UInt32

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

def Cli.ExtendableCmd.subCmds : Cli.ExtendableCmd → Array Cli.ExtendableCmd

Subcommands. May be mutated by extensions.

Equations

• (Cli.ExtendableCmd.init v run subCmds originalFullName?).subCmds = subCmds

def Cli.ExtendableCmd.update' (c : Cli.ExtendableCmd) (meta : optParam Cli.Cmd.Meta c.meta) (run : optParam (Cli.Parsed → IO UInt32) c.run) (subCmds : optParam (Array Cli.ExtendableCmd) c.subCmds) : Cli.ExtendableCmd

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)

def Cli.ExtendableCmd.update (c : Cli.ExtendableCmd) (name : optParam String c.meta.name) (version? : optParam (Option String) c.meta.version?) (description : optParam String c.meta.description) (furtherInformation? : optParam (Option String) c.meta.furtherInformation?) (flags : optParam (Array Cli.Flag) c.meta.flags) (positionalArgs : optParam (Array Cli.Arg) c.meta.positionalArgs) (variableArg? : optParam (Option Cli.Arg) c.meta.variableArg?) (run : optParam (Cli.Parsed → IO UInt32) c.run) (subCmds : optParam (Array Cli.ExtendableCmd) c.subCmds) : Cli.ExtendableCmd

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.

def Cli.ExtendableCmd.mk' (meta : Cli.Cmd.Meta) (run : Cli.Parsed → IO UInt32) (subCmds : optParam (Array Cli.ExtendableCmd) #[]) : Cli.ExtendableCmd

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

def Cli.ExtendableCmd.mkWithHelpAndVersionFlags' (meta : Cli.Cmd.Meta) (run : Cli.Parsed → IO UInt32) (subCmds : optParam (Array Cli.ExtendableCmd) #[]) : Cli.ExtendableCmd

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

def Cli.ExtendableCmd.mk (parent : Cli.ExtendableCmd) (name : String) (version? : Option String) (description : String) (furtherInformation? : optParam (Option String) none) (flags : optParam (Array Cli.Flag) #[]) (positionalArgs : optParam (Array Cli.Arg) #[]) (variableArg? : optParam (Option Cli.Arg) none) (run : Cli.Parsed → IO UInt32) (subCmds : optParam (Array Cli.ExtendableCmd) #[]) : Cli.ExtendableCmd

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.

def Cli.ExtendableCmd.mkWithHelpAndVersionFlags (parent : Cli.ExtendableCmd) (name : String) (version? : Option String) (description : String) (furtherInformation? : optParam (Option String) none) (flags : optParam (Array Cli.Flag) #[]) (positionalArgs : optParam (Array Cli.Arg) #[]) (variableArg? : optParam (Option Cli.Arg) none) (run : Cli.Parsed → IO UInt32) (subCmds : optParam (Array Cli.ExtendableCmd) #[]) : Cli.ExtendableCmd

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.

def Cli.ExtendableCmd.name (c : Cli.ExtendableCmd) : String

Name that is displayed in the help.

Equations

• c.name = c.meta.name

def Cli.ExtendableCmd.version? (c : Cli.ExtendableCmd) : Option String

Version of the command that is displayed in the help and when the version is queried.

Equations

• c.version? = c.meta.version?

def Cli.ExtendableCmd.description (c : Cli.ExtendableCmd) : String

Description that is displayed in the help.

Equations

• c.description = c.meta.description

def Cli.ExtendableCmd.furtherInformation? (c : Cli.ExtendableCmd) : Option String

Information appended to the end of the help. Useful for command extensions.

Equations

• c.furtherInformation? = c.meta.furtherInformation?

def Cli.ExtendableCmd.flags (c : Cli.ExtendableCmd) : Array Cli.Flag

Supported flags ("options" in standard terminology).

Equations

• c.flags = c.meta.flags

def Cli.ExtendableCmd.positionalArgs (c : Cli.ExtendableCmd) : Array Cli.Arg

Supported positional arguments ("operands" in standard terminology).

Equations

• c.positionalArgs = c.meta.positionalArgs

def Cli.ExtendableCmd.variableArg? (c : Cli.ExtendableCmd) : Option Cli.Arg

Variable argument after the end of the positional arguments.

Equations

• c.variableArg? = c.meta.variableArg?

def Cli.ExtendableCmd.fullName (c : Cli.ExtendableCmd) : String

Full name from the root to this command, including the name of the command itself.

Equations

• c.fullName = c.meta.fullName

def Cli.ExtendableCmd.version! (c : Cli.ExtendableCmd) : String

Version of the command that is displayed in the help and when the version is queried.

Equations

• c.version! = c.meta.version!

def Cli.ExtendableCmd.furtherInformation! (c : Cli.ExtendableCmd) : String

Information appended to the end of the help. Useful for command extensions.

Equations

• c.furtherInformation! = c.meta.furtherInformation!

def Cli.ExtendableCmd.variableArg! (c : Cli.ExtendableCmd) : Cli.Arg

Variable argument after the end of the positional arguments.

Equations

• c.variableArg! = c.meta.variableArg!

def Cli.ExtendableCmd.hasVersion (c : Cli.ExtendableCmd) : Bool

Checks whether c has a version.

Equations

• c.hasVersion = c.meta.hasVersion

def Cli.ExtendableCmd.hasFurtherInformation (c : Cli.ExtendableCmd) : Bool

Checks whether c has information appended to the end of the help.

Equations

• c.hasFurtherInformation = c.meta.hasFurtherInformation

def Cli.ExtendableCmd.hasVariableArg (c : Cli.ExtendableCmd) : Bool

Checks whether c supports a variable argument.

Equations

• c.hasVariableArg = c.meta.hasVariableArg

def Cli.ExtendableCmd.flag? (c : Cli.ExtendableCmd) (longName : String) : Option Cli.Flag

Finds the flag in c with the corresponding longName.

Equations

• c.flag? longName = c.meta.flag? longName

def Cli.ExtendableCmd.positionalArg? (c : Cli.ExtendableCmd) (name : String) : Option Cli.Arg

Finds the positional argument in c with the corresponding name.

Equations

• c.positionalArg? name = c.meta.positionalArg? name

def Cli.ExtendableCmd.flag! (c : Cli.ExtendableCmd) (longName : String) : Cli.Flag

Finds the flag in c with the corresponding longName.

Equations

• c.flag! longName = c.meta.flag! longName

def Cli.ExtendableCmd.positionalArg! (c : Cli.ExtendableCmd) (name : String) : Cli.Arg

Finds the positional argument in c with the corresponding name.

Equations

• c.positionalArg! name = c.meta.positionalArg! name

def Cli.ExtendableCmd.hasFlag (c : Cli.ExtendableCmd) (longName : String) : Bool

Checks whether c contains a flag with the corresponding longName.

Equations

• c.hasFlag longName = c.meta.hasFlag longName

def Cli.ExtendableCmd.hasPositionalArg (c : Cli.ExtendableCmd) (name : String) : Bool

Checks whether c contains a positional argument with the corresponding name.

Equations

• c.hasPositionalArg name = c.meta.hasPositionalArg name

def Cli.ExtendableCmd.flagByShortName? (c : Cli.ExtendableCmd) (name : String) : Option Cli.Flag

Finds the flag in c with the corresponding shortName.

Equations

• c.flagByShortName? name = c.meta.flagByShortName? name

def Cli.ExtendableCmd.subCmd? (c : Cli.ExtendableCmd) (name : String) : Option Cli.ExtendableCmd

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)

def Cli.ExtendableCmd.flagByShortName! (c : Cli.ExtendableCmd) (name : String) : Cli.Flag

Finds the flag in c with the corresponding shortName.

Equations

• c.flagByShortName! name = c.meta.flagByShortName! name

def Cli.ExtendableCmd.subCmd! (c : Cli.ExtendableCmd) (name : String) : Cli.ExtendableCmd

Finds the subcommand in c with the corresponding name.

Equations

• c.subCmd! name = (c.subCmd? name).get!

def Cli.ExtendableCmd.hasFlagByShortName (c : Cli.ExtendableCmd) (name : String) : Bool

Checks whether c has a flag with the corresponding shortName.

Equations

• c.hasFlagByShortName name = c.meta.hasFlagByShortName name

def Cli.ExtendableCmd.hasSubCmd (c : Cli.ExtendableCmd) (name : String) : Bool

Checks whether c contains a subcommand with the corresponding name.

Equations

• c.hasSubCmd name = (c.subCmd? name).isSome

structure Cli.Extension : Type

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 the ExtendableCmd that results from all extensions being applied. If postprocessing mutates the subcommand structure in Parsed.cmd, care must be taken to update Parsed.parent? accordingly as well.

instance Cli.instInhabitedExtension : Inhabited Cli.Extension

Equations

• Cli.instInhabitedExtension = { default := { priority := default, extend := default, postprocess := default } }

def Cli.Extension.then (a : Cli.Extension) (b : Cli.Extension) : Cli.Extension

Composes both extensions so that the Cmds 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.

inductive Cli.Cmd : Type

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

instance Cli.instInhabitedCmd : Inhabited Cli.Cmd

Equations

• Cli.instInhabitedCmd = { default := Cli.Cmd.init default default default default }

def Cli.Cmd.meta : Cli.Cmd → Cli.Cmd.Meta

Non-recursive meta-data.

Equations

• (Cli.Cmd.init v run subCmds extension?).meta = v

def Cli.Cmd.run : Cli.Cmd → Cli.Parsed → IO UInt32

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

def Cli.Cmd.subCmds : Cli.Cmd → Array Cli.Cmd

Subcommands.

Equations

• (Cli.Cmd.init v run subCmds extension?).subCmds = subCmds

def Cli.Cmd.extension? : Cli.Cmd → Option Cli.Extension

Extension of the Cli library.

Equations

• (Cli.Cmd.init v run subCmds extension?).extension? = extension?

def Cli.Cmd.updateParentNames (c : Cli.Cmd) : Cli.Cmd

Recomputes all the parent names of subcommands in c with c as the root command.

Equations

• c.updateParentNames = Cli.Cmd.updateParentNames.loop c #[]

partial def Cli.Cmd.updateParentNames.loop (c : Cli.Cmd) (parentNames : Array String) : Cli.Cmd

def Cli.Cmd.mk' (meta : Cli.Cmd.Meta) (run : Cli.Parsed → IO UInt32) (subCmds : optParam (Array Cli.Cmd) #[]) (extension? : optParam (Option Cli.Extension) none) : Cli.Cmd

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

def Cli.Cmd.mk (name : String) (version? : Option String) (description : String) (furtherInformation? : optParam (Option String) none) (flags : optParam (Array Cli.Flag) #[]) (positionalArgs : optParam (Array Cli.Arg) #[]) (variableArg? : optParam (Option Cli.Arg) none) (run : Cli.Parsed → IO UInt32) (subCmds : optParam (Array Cli.Cmd) #[]) (extension? : optParam (Option Cli.Extension) none) : Cli.Cmd

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.

def Cli.Cmd.subCmd? (c : Cli.Cmd) (name : String) : Option Cli.Cmd

Finds the subcommand in c with the corresponding name.

Equations

• c.subCmd? name = c.subCmds.find? fun (x : Cli.Cmd) => decide (x.meta.name = name)

def Cli.Cmd.extension! (c : Cli.Cmd) : Cli.Extension

Extension of the Cli library.

Equations

• c.extension! = c.extension?.get!

def Cli.Cmd.subCmd! (c : Cli.Cmd) (name : String) : Cli.Cmd

Finds the subcommand in c with the corresponding name.

Equations

• c.subCmd! name = (c.subCmd? name).get!

def Cli.Cmd.hasSubCmd (c : Cli.Cmd) (name : String) : Bool

Checks whether c contains a subcommand with the corresponding name.

Equations

• c.hasSubCmd name = (c.subCmd? name).isSome

def Cli.Cmd.hasExtension (c : Cli.Cmd) : Bool

Checks whether c is being extended.

Equations

• c.hasExtension = c.extension?.isSome

partial def Cli.Parsed.Cmd.ofFullCmd (c : Cli.Cmd) : Cli.Parsed.Cmd

Extracts meta and the recursive subcommand structure from c to create a Parsed.Cmd.

partial def Cli.Parsed.Cmd.toFullCmd (c : Cli.Parsed.Cmd) : Cli.Cmd

Embeds c into a Cli.Cmd that does nothing.

def Cli.Parsed.toCmd (p : Cli.Parsed) : Cli.Cmd

Embeds p.cmd into a Cli.Cmd that does nothing.

Equations

• p.toCmd = p.cmd.toFullCmd

partial def Cli.ExtendableCmd.ofFullCmd (c : Cli.Cmd) : Cli.ExtendableCmd

Creates a view of c that can be extended by extensions.

def Cli.ExtendableCmd.toFullCmd (c : Cli.ExtendableCmd) (original : Cli.Cmd) : Cli.Cmd

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.

partial def Cli.ExtendableCmd.toFullCmd.loop (extensionIndex : Lean.RBMap String (Option Cli.Extension) compare) (c : Cli.ExtendableCmd) : Cli.Cmd

partial def Cli.ExtendableCmd.toFullCmd.collectExtensions (currentCmd : Cli.Cmd) : Array (String × Option Cli.Extension)

partial def Cli.ExtendableCmd.toFullCmd.prependOriginalParentNames (original : Cli.Cmd) (currentCmd : Cli.Cmd) : Cli.Cmd

partial def Cli.ExtendableCmd.toFullCmdWithoutExtensions (c : Cli.ExtendableCmd) : Cli.Cmd

Converts c back into Cli.Cmd while retaining none of the extensions.

def Cli.literalIdent : Lean.ParserDescr

Equations

• Cli.literalIdent = Lean.ParserDescr.nodeWithAntiquot "literalIdent" `Cli.literalIdent (Lean.ParserDescr.cat `term 0)

def Cli.runFun : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cli.positionalArg : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cli.variableArg : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cli.flag : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cli.«term`[Cli|__;[_]_FLAGS:_ARGS:__SUBCOMMANDS:_;;EXTENSIONS:_;;]» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cli.expandIdentLiterally (t : Lean.Term) : Lean.Term

Equations

• One or more equations did not get rendered due to their size.

def Cli.expandRunFun (runFun : Lean.TSyntax `Cli.runFun) : Lean.MacroM Lean.Term

Equations

• One or more equations did not get rendered due to their size.

def Cli.expandPositionalArg (positionalArg : Lean.TSyntax `Cli.positionalArg) : Lean.MacroM Lean.Term

Equations

• One or more equations did not get rendered due to their size.

def Cli.expandVariableArg (variableArg : Lean.TSyntax `Cli.variableArg) : Lean.MacroM Lean.Term

Equations

• One or more equations did not get rendered due to their size.

def Cli.expandFlag (flag : Lean.TSyntax `Cli.flag) : Lean.MacroM Lean.Term

Equations

• One or more equations did not get rendered due to their size.

def Cli.maxWidth : Nat

Maximum width within which all formatted text should fit.

Equations

• Cli.maxWidth = 80

def Cli.indentation : Nat

Amount of spaces with which section content is indented.

Equations

• Cli.indentation = 4

def Cli.maxIndentedWidth : Nat

Maximum width within which all formatted text should fit, after indentation.

Equations

• Cli.maxIndentedWidth = Cli.maxWidth - Cli.indentation

def Cli.line (xs : Array String) : String

Formats xs by String.optJoining the components with a single space.

Equations

• Cli.line xs = Cli.String.optJoin xs " "

def Cli.lines (xs : Array String) : String

Formats xs by String.optJoining the components with a newline \n.

Equations

• Cli.lines xs = Cli.String.optJoin xs "\n"

def Cli.renderSection (title : String) (content : String) (emptyContentPlaceholder? : optParam (Option String) none) : String

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.

def Cli.renderTable (title : String) (columns : Array (String × String)) (emptyTablePlaceholder? : optParam (Option String) none) : String

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?

def Cli.Cmd.help (c : Cli.Cmd) : String

Renders the help for c.

Equations

• One or more equations did not get rendered due to their size.

def Cli.Cmd.error (c : Cli.Cmd) (msg : String) : String

Renders an error for c with the designated message msg.

Equations

• One or more equations did not get rendered due to their size.

def Cli.Cmd.printHelp (c : Cli.Cmd) : IO Unit

Prints the help for c.

Equations

• c.printHelp = IO.println c.help

def Cli.Cmd.printError (c : Cli.Cmd) (msg : String) : IO Unit

Prints an error for c with the designated message msg.

Equations

• c.printError msg = IO.eprintln (c.error msg)

def Cli.Cmd.printVersion! (c : Cli.Cmd) : IO Unit

Prints the version of c. Panics if c has no version.

Equations

• c.printVersion! = IO.println c.meta.version!

def Cli.Parsed.help (p : Cli.Parsed) : String

Renders the help for p.cmd.

Equations

• p.help = p.toCmd.help

def Cli.Parsed.error (p : Cli.Parsed) (msg : String) : String

Renders an error for p.cmd with the designated message msg.

Equations

• p.error msg = p.toCmd.error msg

def Cli.Parsed.printHelp (p : Cli.Parsed) : IO Unit

Prints the help for p.cmd.

Equations

• p.printHelp = p.toCmd.printHelp

def Cli.Parsed.printError (p : Cli.Parsed) (msg : String) : IO Unit

Prints an error for p.cmd with the designated message msg.

Equations

• p.printError msg = p.toCmd.printError msg

def Cli.Parsed.printVersion! (p : Cli.Parsed) : IO Unit

Prints the version of p.cmd. Panics if p.cmd has no version.

Equations

• p.printVersion! = p.toCmd.printVersion!

structure Cli.InputFlag : Type

Represents the exact representation of a flag as input by the user.

• name : String

  Flag name input by the user.

• isShort : Bool

  Whether the flag input by the user was a short one.

instance Cli.instToStringInputFlag : ToString Cli.InputFlag

Equations

• One or more equations did not get rendered due to their size.

inductive Cli.ParseError.Kind : Type

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

def Cli.ParseError.Kind.msg : Cli.ParseError.Kind → String

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

structure Cli.ParseError : Type

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.

def Cli.Cmd.parse (c : Cli.Cmd) (args : List String) : Except Cli.ParseError (Cli.Cmd × Cli.Parsed)

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

partial def Cli.Cmd.applyExtensions (c : Cli.Cmd) : Cli.Cmd

Recursively applies extensions in all subcommands in c bottom-up and c itself.

def Cli.Cmd.process (c : Cli.Cmd) (args : List String) : Except (Cli.Cmd × String) (Cli.Cmd × Cli.Parsed)

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.

def Cli.Cmd.validate (c : Cli.Cmd) (args : List String) : IO UInt32

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.