def Options.Applicative.long (name : String) : Mod

Set the long option name (e.g., "output" for --output). $$\text{long} : \text{String} \to \text{Mod}$$

Equations

• Options.Applicative.long name = { long := some name }

def Options.Applicative.short (c : Char) : Mod

Set the short option character (e.g., 'o' for -o). $$\text{short} : \text{Char} \to \text{Mod}$$

Equations

• Options.Applicative.short c = { short := some c }

def Options.Applicative.help (text : String) : Mod

Set the help text for an option. $$\text{help} : \text{String} \to \text{Mod}$$

Equations

• Options.Applicative.help text = { help := some text }

def Options.Applicative.metavar (name : String) : Mod

Set the metavar for an option (displayed in usage, e.g., FILE). $$\text{metavar} : \text{String} \to \text{Mod}$$

Equations

• Options.Applicative.metavar name = { metavar := some name }

def Options.Applicative.hidden : Mod

Mark an option as hidden from help output. $$\text{hidden} : \text{Mod}$$

Equations

• Options.Applicative.hidden = { hidden := true }

def Options.Applicative.showDefault : Mod

Mark that the default value should be shown in help. $$\text{showDefault} : \text{Mod}$$

Equations

• Options.Applicative.showDefault = { showDefault := true }

def Options.Applicative.str : ReadM String

Identity reader that returns the string as-is. $$\text{str} : \text{ReadM String}$$

Equations

• Options.Applicative.str s = Except.ok s

def Options.Applicative.eitherReader {α : Type} (f : String → Except String α) : ReadM α

Construct a reader from an Except-returning function. $$\text{eitherReader} : (\text{String} \to \text{Except String}\ \alpha) \to \text{ReadM}\ \alpha$$

Equations

• Options.Applicative.eitherReader f = f

class Options.Applicative.FromString (α : Type) : Type

A class for types that can be parsed from a string representation. Used by the auto reader.

• fromString? : String → Option α

  Parse a string into a value, or return none on failure.

@[implicit_reducible]

instance Options.Applicative.instFromStringString : FromString String

Equations

• Options.Applicative.instFromStringString = { fromString? := fun (s : String) => some s }

@[implicit_reducible]

instance Options.Applicative.instFromStringNat : FromString Nat

Equations

• Options.Applicative.instFromStringNat = { fromString? := fun (s : String) => s.toNat? }

@[implicit_reducible]

instance Options.Applicative.instFromStringInt : FromString Int

Equations

• Options.Applicative.instFromStringInt = { fromString? := fun (s : String) => s.toInt? }

@[implicit_reducible]

instance Options.Applicative.instFromStringBool : FromString Bool

Equations

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

def Options.Applicative.auto {α : Type} [ToString α] [FromString α] : ReadM α

Automatic reader using FromString and ToString instances. $$\text{auto} : [\text{ToString}\ \alpha] \to [\text{FromString}\ \alpha] \to \text{ReadM}\ \alpha$$

Equations

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

def Options.Applicative.option {α : Type} (reader : ReadM α) (mods : Mod) : Parser α

Build a typed option using the given reader. The option can appear anywhere in the argument list (scanned). $$\text{option} : \text{ReadM}\ \alpha \to \text{Mod} \to \text{Parser}\ \alpha$$

Equations

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

def Options.Applicative.strOption (mods : Mod) : Parser String

Build a string-valued option. $$\text{strOption} : \text{Mod} \to \text{Parser String}$$

Equations

• Options.Applicative.strOption mods = Options.Applicative.option Options.Applicative.str mods

def Options.Applicative.switch (mods : Mod) : Parser Bool

Build a boolean switch (defaults to false, active when present). $$\text{switch} : \text{Mod} \to \text{Parser Bool}$$

Equations

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

def Options.Applicative.flag {α : Type} (inactive active : α) (mods : Mod) : Parser α

Build a flag with explicit inactive/active values. $$\text{flag} : \alpha \to \alpha \to \text{Mod} \to \text{Parser}\ \alpha$$

Equations

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

def Options.Applicative.flag' {α : Type} (active : α) (mods : Mod) : Parser α

Build a flag with no default (must be explicitly provided or combined with alternative). $$\text{flag'} : \alpha \to \text{Mod} \to \text{Parser}\ \alpha$$

Equations

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

def Options.Applicative.argument {α : Type} (reader : ReadM α) (mods : Mod) : Parser α

Build a positional argument parser. Consumes the first non-flag argument. $$\text{argument} : \text{ReadM}\ \alpha \to \text{Mod} \to \text{Parser}\ \alpha$$

Equations

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

def Options.Applicative.argument.findArg {α : Type} (reader : ReadM α) (mods : Mod) (before : List String) : List String → Except String (α × List String)

Equations

• One or more equations did not get rendered due to their size.
• Options.Applicative.argument.findArg reader mods before [] = Except.error (toString "Missing required argument: " ++ toString (mods.metavar.getD "ARG"))

def Options.Applicative.subparser {α : Type} (cmds : List (String × ParserInfo α)) : Parser α

Build a subcommand parser. The first positional argument selects the command. $$\text{subparser} : \text{List (String} \times \text{ParserInfo}\ \alpha\text{)} \to \text{Parser}\ \alpha$$

Equations

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

@[implicit_reducible]

instance Options.Applicative.instPureParser : Pure Parser

Applicative pure: a parser that always succeeds with the given value, consuming no arguments. $$\text{pure} : \alpha \to \text{Parser}\ \alpha$$

Equations

• Options.Applicative.instPureParser = { pure := fun {α : Type} (a : α) => { run := fun (args : List String) => Except.ok (a, args) } }

@[implicit_reducible]

instance Options.Applicative.instFunctorParser : Functor Parser

Functor map for Parser. $$\text{map} : (\alpha \to \beta) \to \text{Parser}\ \alpha \to \text{Parser}\ \beta$$

Equations

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

@[implicit_reducible]

instance Options.Applicative.instSeqParser : Seq Parser

Applicative sequencing for Parser. $$\text{seq} : \text{Parser}\ (\alpha \to \beta) \to (\text{Unit} \to \text{Parser}\ \alpha) \to \text{Parser}\ \beta$$

Equations

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

@[implicit_reducible]

instance Options.Applicative.instSeqLeftParser : SeqLeft Parser

SeqLeft for Parser.

Equations

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

@[implicit_reducible]

instance Options.Applicative.instSeqRightParser : SeqRight Parser

SeqRight for Parser.

Equations

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

@[implicit_reducible]

instance Options.Applicative.instApplicativeParser : Applicative Parser

Applicative instance for Parser.

Equations

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

@[implicit_reducible]

instance Options.Applicative.instOrElseParser {α : Type} : OrElse (Parser α)

Alternative: try left parser, fall back to right on failure. $$\text{orElse} : \text{Parser}\ \alpha \to (\text{Unit} \to \text{Parser}\ \alpha) \to \text{Parser}\ \alpha$$

Equations

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

def Options.Applicative.withDefault {α : Type} (dflt : α) (p : Parser α) : Parser α

Set a default value for a parser: if it fails, return the default. $$\text{value} : \alpha \to \text{Parser}\ \alpha \to \text{Parser}\ \alpha$$

Equations

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

def Options.Applicative.optionWithDefault {α : Type} (reader : ReadM α) (mods : Mod) (dflt : α) : Parser α

Build a typed option with a default value. $$\text{optionWithDefault} : \text{ReadM}\ \alpha \to \text{Mod} \to \alpha \to \text{Parser}\ \alpha$$

Equations

• Options.Applicative.optionWithDefault reader mods dflt = Options.Applicative.withDefault dflt (Options.Applicative.option reader mods)

def Options.Applicative.strOptionWithDefault (mods : Mod) (dflt : String) : Parser String

Build a string-valued option with a default value. $$\text{strOptionWithDefault} : \text{Mod} \to \text{String} \to \text{Parser String}$$

Equations

• Options.Applicative.strOptionWithDefault mods dflt = Options.Applicative.withDefault dflt (Options.Applicative.strOption mods)

def Options.Applicative.command {α : Type} (name : String) (info : ParserInfo α) : String × ParserInfo α

Create a command entry for use with subparser. $$\text{command} : \text{String} \to \text{ParserInfo}\ \alpha \to (\text{String} \times \text{ParserInfo}\ \alpha)$$

Equations

• Options.Applicative.command name info = (name, info)