def Options.Applicative.ReadM (α : Type) : Type

A reader that can parse a string value into a typed result. $$\text{ReadM}\ \alpha := \text{String} \to \text{Except String}\ \alpha$$

Equations

• Options.Applicative.ReadM α = (String → Except String α)

@[implicit_reducible]

instance Options.Applicative.instInhabitedReadM {α : Type} : Inhabited (ReadM α)

Equations

• Options.Applicative.instInhabitedReadM = { default := fun (x : String) => Except.error "no reader" }

structure Options.Applicative.Mod : Type

Option visibility and characteristics. Combines long/short names, help text, metavar, and visibility.

• long : Option String

  Long option name (e.g., "output" for --output).

• short : Option Char

  Short option character (e.g., 'o' for -o).

• help : Option String

  Help text displayed in usage.

• metavar : Option String

  Metavar displayed in usage (e.g., FILE in --output FILE).

• hidden : Bool

  Whether this option is hidden from help.

• showDefault : Bool

  Whether to show the default value in help text.

def Options.Applicative.instInhabitedMod.default : Mod

Equations

• Options.Applicative.instInhabitedMod.default = { long := default, short := default, help := default, metavar := default, hidden := default, showDefault := default }

@[implicit_reducible]

instance Options.Applicative.instInhabitedMod : Inhabited Mod

Equations

• Options.Applicative.instInhabitedMod = { default := Options.Applicative.instInhabitedMod.default }

def Options.Applicative.instReprMod.repr : Mod → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Options.Applicative.instReprMod : Repr Mod

Equations

• Options.Applicative.instReprMod = { reprPrec := Options.Applicative.instReprMod.repr }

@[implicit_reducible]

instance Options.Applicative.instAppendMod : Append Mod

Combine two Mod values, with the right-hand side taking precedence for fields that are set.

Equations

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

structure Options.Applicative.InfoMod : Type

Modifier configuration for ParserInfo. $$\text{InfoMod} := \text{ParserInfo-level modifiers}$$

• description : Option String

  Program description.

• header : Option String

  Header text shown before usage.

• footer : Option String

  Footer text shown after options.

• fullDesc : Bool

  Whether to show full description in help.

• failureCode : Nat

  Exit code on parse failure.

@[implicit_reducible]

instance Options.Applicative.instInhabitedInfoMod : Inhabited InfoMod

Equations

• Options.Applicative.instInhabitedInfoMod = { default := Options.Applicative.instInhabitedInfoMod.default }

def Options.Applicative.instInhabitedInfoMod.default : InfoMod

Equations

• Options.Applicative.instInhabitedInfoMod.default = { description := default, header := default, footer := default, fullDesc := default, failureCode := default }

def Options.Applicative.instReprInfoMod.repr : InfoMod → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Options.Applicative.instReprInfoMod : Repr InfoMod

Equations

• Options.Applicative.instReprInfoMod = { reprPrec := Options.Applicative.instReprInfoMod.repr }

inductive Options.Applicative.OptDescr : Type

Description of a single option, used for generating help text. Separated from the parsing logic so that the parser can be a plain function type.

• optionDescr (mods : Mod) : OptDescr

  A named option (--long / -s).

• flagDescr (mods : Mod) : OptDescr

  A flag (--long / -s, no value).

• argDescr (mods : Mod) : OptDescr

  A positional argument.

• cmdDescr (commands : List (String × Option String)) : OptDescr

  A subcommand group.

def Options.Applicative.instInhabitedOptDescr.default : OptDescr

Equations

• Options.Applicative.instInhabitedOptDescr.default = Options.Applicative.OptDescr.optionDescr default

@[implicit_reducible]

instance Options.Applicative.instInhabitedOptDescr : Inhabited OptDescr

Equations

• Options.Applicative.instInhabitedOptDescr = { default := Options.Applicative.instInhabitedOptDescr.default }

def Options.Applicative.instReprOptDescr.repr : OptDescr → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Options.Applicative.instReprOptDescr : Repr OptDescr

Equations

• Options.Applicative.instReprOptDescr = { reprPrec := Options.Applicative.instReprOptDescr.repr }

structure Options.Applicative.Parser (α : Type) : Type

A composable command-line parser. Internally a function from an argument list to either an error or a pair of (parsed value, remaining args). Option descriptions are tracked separately for help generation.

$$\text{Parser}\ \alpha := \{ \text{run} : \text{List String} \to \text{Except String}\ (\alpha \times \text{List String}), \text{descrs} : \text{List OptDescr} \}$$

• run : List String → Except String (α × List String)

  Run the parser on an argument list, returning the result and remaining args.

• descrs : List OptDescr

  Option descriptions for help text generation.

structure Options.Applicative.ParserInfo (α : Type) : Type

Parser with metadata for help text generation. $$\text{ParserInfo}\ \alpha := (\text{Parser}\ \alpha, \text{description}, \text{header}, \text{footer}, \ldots)$$

• parser : Parser α

  The underlying parser.

• description : Option String

  Program description.

• header : Option String

  Header text shown before usage.

• footer : Option String

  Footer text shown after options.

• fullDesc : Bool

  Whether to show full description.

• failureCode : Nat

  Exit code on parse failure.