def Cli.Array.leftUnionBy {α : Type u_1} {β : Type u_2} [Ord α] (key : β → α) (left : Array β) (right : Array β) : Array β

Appends those elements of right to left whose key is not already contained in left.

Equations

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

def Cli.Array.rightUnionBy {α : Type u_1} {β : Type u_2} [Ord α] (key : β → α) (left : Array β) (right : Array β) : Array β

Prepends those elements of left to right whose key is not already contained in right.

Equations

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

def Cli.Array.diffBy {α : Type u_1} {β : Type u_2} [Ord α] (key : β → α) (left : Array β) (right : Array α) : Array β

Deletes all elements from left whose key is in right.

Equations

• Cli.Array.diffBy key left right = Array.filter (fun (v : β) => decide ¬(Lean.RBTree.ofList right.toList).contains (key v) = true) left

def Cli.author (author : String) : Cli.Extension

Prepends an author name to the description of the command.

Equations

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

def Cli.longDescription (description : String) : Cli.Extension

Appends a longer description to the end of the help.

Equations

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

def Cli.helpSubCommand : Cli.Extension

Adds a help subcommand.

Equations

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

def Cli.versionSubCommand! : Cli.Extension

Adds a version subcommand.

Equations

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

def Cli.defaultValues! (defaults : Array (String × String)) : Cli.Extension

Sets default values for flags that were not set by the user according to defaults := #[(long flag name, default value), ...] and denotes the default value in the flag description of the help. Panics if one of the designated long flag names cannot be found in the command.

Equations

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

def Cli.require! (requiredFlags : Array String) : Cli.Extension

Errors if one of requiredFlags := #[long flag name, ...] were not passed by the user. Denotes that the flag is required in the flag description of the help. Panics if one of the designated long flag names cannot be found in the command.

Equations

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