def Options.Applicative.renderHelp {α : Type} (pinfo : ParserInfo α) : String

Generate help text for a ParserInfo. $$\text{renderHelp} : \text{ParserInfo}\ \alpha \to \text{String}$$

Equations

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

def Options.Applicative.helper {α : Type} : Parser (α → α)

A parser that recognises --help / -h and returns the identity function. When combined with <*>, it passes through the original value unchanged. $$\text{helper} : \text{Parser}\ (\alpha \to \alpha)$$

Equations

• Options.Applicative.helper = Options.Applicative.flag id id { long := some "help", short := some 'h', help := some "Show this help text" }

def Options.Applicative.info {α : Type} (p : Parser α) (mods : InfoMod := { }) : ParserInfo α

Wrap a parser with info metadata. $$\text{info} : \text{Parser}\ \alpha \to \text{InfoMod} \to \text{ParserInfo}\ \alpha$$

Equations

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

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

Build a hidden subparser (not shown in help). $$\text{hsubparser} : \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.

def Options.Applicative.execParser {α : Type} (pinfo : ParserInfo α) (args : List String) : IO α

Parse the given argument list using the ParserInfo, printing help and exiting on failure or when --help is requested.

Intended to be called from main:

def main (args : List String) : IO Unit := do
  let opts ← execParser myParserInfo args
  ...

$$\text{execParser} : \text{ParserInfo}\ \alpha \to \text{List String} \to \text{IO}\ \alpha$$

Equations

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

def Options.Applicative.execParserPure {α : Type} (pinfo : ParserInfo α) (args : List String) : Except String α

Pure variant of execParser that returns an Except instead of performing IO. Useful for testing. $$\text{execParserPure} : \text{ParserInfo}\ \alpha \to \text{List String} \to \text{Except String}\ \alpha$$

Equations

• Options.Applicative.execParserPure pinfo args = match pinfo.parser.run args with | Except.ok (result, snd) => Except.ok result | Except.error e => Except.error e