Recursive Parsing for Options🔗

If your tool takes multiple options in any order, a recursive function that builds up a configuration structure is recommended.

structure CliConfig where
  verbose : Bool := false
  outputFile : Option String := none
  inputFiles : List String := []
deriving Repr

/-- Recursively parses arguments
  into a CliConfig structure. -/
partial def parseConfig (args : List String)
  (cfg : CliConfig := {}) : CliConfig :=
  match args with
  | [] => cfg
  | "-v" :: rest | "--verbose" :: rest =>
    parseConfig rest { cfg with verbose := true }
  | "-o" :: file :: rest | "--output" :: file :: rest =>
    parseConfig rest { cfg with outputFile := some file }
  | file :: rest =>
    parseConfig rest { cfg with inputFiles :=
      cfg.inputFiles ++ [file] }

def runParser (args : List String) : IO Unit := do
  let cfg := parseConfig args
  IO.println s!"Configuration: {repr cfg}"

For a better and more robust tool, refer Lean4-cli for a more comprehensive command-line parsing library.