diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean
index 03ad8b543d..ec82e77983 100644
--- a/Lake/CLI/Main.lean
+++ b/Lake/CLI/Main.lean
@@ -11,7 +11,7 @@ import Lake.Config.Resolve
 import Lake.Config.Util
 import Lake.Util.Error
 import Lake.Util.MainM
-import Lake.Util.CliT
+import Lake.Util.Cli
 import Lake.CLI.Init
 import Lake.CLI.Help
 import Lake.CLI.Build
@@ -23,7 +23,7 @@ namespace Lake
 
 -- # CLI
 
-structure CliState where
+structure LakeOptions where
   rootDir : FilePath := "."
   configFile : FilePath := defaultConfigFile
   leanInstall? : Option LeanInstall := none
@@ -31,65 +31,65 @@ structure CliState where
   subArgs : List String := []
   wantsHelp : Bool := false
 
-abbrev CliM := CliT <| StateT CliState MainM
+abbrev CliStateM := StateT LakeOptions <| MainM
+abbrev CliM := ArgsT CliStateM
 
 namespace Cli
-open CliT
 
 -- ## Basic Actions
 
 /-- Print out a line wih the given message and then exit with an error code. -/
-protected def error (msg : String) (rc : UInt32 := 1) : CliM α := do
+protected def error (msg : String) (rc : UInt32 := 1) : MainM α := do
   IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => ()
   exit rc
 
-instance : MonadError CliM := ⟨Cli.error⟩
-instance : MonadLift IO CliM := ⟨MonadError.runIO⟩
+instance : MonadError MainM := ⟨Cli.error⟩
+instance : MonadLift IO MainM := ⟨MonadError.runIO⟩
 
--- ## State Management
+-- ## Basic State Management
 
-def getRootDir : CliM FilePath :=
-  (·.rootDir) <$> getThe CliState
+def getRootDir : CliStateM FilePath :=
+  (·.rootDir) <$> get
 
-def setRootDir (dir : FilePath) : CliM PUnit :=
-  modifyThe CliState fun st => {st with rootDir := dir}
+def setRootDir (dir : FilePath) : CliStateM PUnit :=
+  modify fun st => {st with rootDir := dir}
 
-def getConfigFile : CliM FilePath :=
-  (·.configFile) <$> getThe CliState
+def getConfigFile : CliStateM FilePath :=
+  (·.configFile) <$> get
 
-def setConfigFile (file : FilePath) : CliM PUnit :=
-  modifyThe CliState fun st => {st with configFile := file}
+def setConfigFile (file : FilePath) : CliStateM PUnit :=
+  modify ({· with configFile := file})
 
-def getSubArgs : CliM (List String) :=
-  (·.subArgs) <$> getThe CliState
+def getSubArgs : CliStateM (List String) :=
+  (·.subArgs) <$> get
 
-def setSubArgs (args : List String) : CliM PUnit :=
-  modifyThe CliState fun st => {st with subArgs := args}
+def setSubArgs (args : List String) : CliStateM PUnit :=
+  modify fun st => {st with subArgs := args}
 
-def getWantsHelp : CliM Bool :=
-  (·.wantsHelp) <$> getThe CliState
+def getWantsHelp : CliStateM Bool :=
+  (·.wantsHelp) <$> get
 
-def setWantsHelp : CliM PUnit :=
-  modifyThe CliState fun st => {st with wantsHelp := true}
+def setWantsHelp : CliStateM PUnit :=
+  modify fun st => {st with wantsHelp := true}
 
-def setLean (lean : String) : CliM PUnit := do
+def setLean (lean : String) : CliStateM PUnit := do
   let leanInstall? ← findLeanCmdInstall? lean
-  modifyThe CliState fun st => {st with leanInstall?}
+  modify fun st => {st with leanInstall?}
 
-def getLeanInstall? : CliM (Option LeanInstall) :=
-  (·.leanInstall?) <$> getThe CliState
+def getLeanInstall? : CliStateM (Option LeanInstall) :=
+  (·.leanInstall?) <$> get
 
-def getLakeInstall? : CliM (Option LakeInstall) :=
-  (·.lakeInstall?) <$> getThe CliState
+def getLakeInstall? : CliStateM (Option LakeInstall) :=
+  (·.lakeInstall?) <$> get
 
--- ## Complex Actions
+-- ## Complex State Management
 
-def loadPkg (args : List String := []) : CliM Package := do
+def loadPkg (args : List String := []) : CliStateM Package := do
   let dir ← getRootDir; let file ← getConfigFile
   setupLeanSearchPath (← getLeanInstall?) (← getLakeInstall?)
   Package.load dir args (dir / file)
 
-def loadConfig (args : List String := []) : CliM (Workspace × Package) := do
+def loadConfig (args : List String := []) : CliStateM (Workspace × Package) := do
   let pkg ← loadPkg args
   let ws ← Workspace.ofPackage pkg
   let packageMap ← resolveDeps ws pkg |>.run LogMethods.eio (m := IO)
@@ -97,31 +97,31 @@ def loadConfig (args : List String := []) : CliM (Workspace × Package) := do
   ({ws with packageMap}, pkg)
 
 /-- Get the Lean installation. Error if missing. -/
-def getLeanInstall : CliM LeanInstall := do
+def getLeanInstall : CliStateM LeanInstall := do
   if let some leanInstall ← getLeanInstall? then
     return leanInstall
   else
     error "could not detect a Lean installation"
 
 /-- Get the Lake installation. Error if missing. -/
-def getLakeInstall : CliM LakeInstall := do
+def getLakeInstall : CliStateM LakeInstall := do
   if let some lakeInstall ← getLakeInstall? then
     return lakeInstall
   else
     error "could not detect the configuration of the Lake installation"
 
 /-- Get the Lean and Lake installation. Error if either is missing. -/
-def getInstall : CliM (LeanInstall × LakeInstall) := do
+def getInstall : CliStateM (LeanInstall × LakeInstall) := do
   return (← getLeanInstall, ← getLakeInstall)
 
 /-- Perform the given build action using information from CLI. -/
-def runBuildM (ws : Workspace) (x : BuildM α) : CliM α := do
+def runBuildM (ws : Workspace) (x : BuildM α) : CliStateM α := do
   let (leanInstall, lakeInstall) ← getInstall
   let ctx ← mkBuildContext ws leanInstall lakeInstall
   x.run LogMethods.io ctx
 
 /-- Variant of `runBuildM` that discards the build monad's output. -/
-def runBuildM_ (ws : Workspace) (x : BuildM α) : CliM PUnit :=
+def runBuildM_ (ws : Workspace) (x : BuildM α) : CliStateM PUnit :=
   discard <| runBuildM ws x
 
 -- ## Argument Parsing
@@ -135,7 +135,7 @@ def takeArg (errMsg : String := "missing argument") : CliM String := do
 Verify that there are no CLI arguments remaining
 before running the given action.
 -/
-def noArgsRem (act : CliM α) : CliM α := do
+def noArgsRem (act : CliStateM α) : CliM α := do
   let args ← getArgs
   if args.isEmpty then act else
     error s!"unexpected arguments: {" ".intercalate args}"
@@ -162,29 +162,25 @@ def longOption : (opt : String) → CliM PUnit
 | "--"      => do setSubArgs <| ← takeArgs
 | opt       => unknownLongOption opt
 
-/-- Splits a long option of the form `--long=arg` into `--long arg`. -/
-def longOptionOrEq (optStr : String) : CliM PUnit :=
-  let eqPos := optStr.posOf '='
-  let arg := optStr.drop eqPos.succ
-  let opt := optStr.take eqPos
-  if arg.isEmpty then
-    longOption opt
-  else do
-    consArg arg
-    longOption opt
+def lakeOption :=
+  option {
+    short := shortOption
+    long := longOption
+    longShort := shortOptionWithArg shortOption
+  }
 
 -- ## Commands
 
-def withPackage [MonadLiftT m CliM] (x : Package → LakeT m α) : CliM α := do
+def withPackage [MonadLiftT m CliStateM] (x : Package → LakeT m α) : CliStateM α := do
   let (ws, pkg) ← loadConfig
   let (lean, lake) ← getInstall
   liftM <| x pkg |>.run {lean, lake, opaqueWs := ws}
 
-def withContext [MonadLiftT m CliM] (x : LakeT m α) : CliM α :=
+def withContext [MonadLiftT m CliStateM] (x : LakeT m α) : CliStateM α :=
   withPackage fun _ => x
 
 /-- Run the given script from the given package with the given arguments. -/
-def script (pkg : Package) (name : String) (args : List String) :  CliM PUnit := do
+def script (pkg : Package) (name : String) (args : List String) : CliStateM PUnit := do
   if let some script := pkg.scripts.find? name then
     if (← getWantsHelp) then
       if let some help := script.help? then
@@ -194,19 +190,19 @@ def script (pkg : Package) (name : String) (args : List String) :  CliM PUnit :=
     else
       exit <| ← withContext <| script.run args
   else
-    pkg.scripts.forM (m := CliM) fun name _ => do
+    pkg.scripts.forM (m := CliStateM) fun name _ => do
       IO.println <| name.toString (escape := false)
     error s!"unknown script '{name}'"
 
 /-- Verify the Lean version Lake was built with matches that of the Lean installation. -/
-def verifyLeanVersion : CliM PUnit := do
+def verifyLeanVersion : CliStateM PUnit := do
   let lean ← getLeanInstall
   unless lean.githash == Lean.githash do
     let githash := if lean.githash.isEmpty then  "nothing" else lean.githash
     error s!"expected Lean commit {Lean.githash}, but got {lean.githash}"
 
 /-- Output the detected installs and verify the Lean version. -/
-def verifyInstall : CliM PUnit := do
+def verifyInstall : CliStateM PUnit := do
   IO.println s!"Lean:\n{repr <| ← getLeanInstall?}"
   IO.println s!"Lake:\n{repr <| ← getLakeInstall?}"
   verifyLeanVersion
@@ -221,7 +217,7 @@ If no configuration file exists, exit silently with `noConfigFileCode` (i.e, 2).
 
 The `print-paths` command is used internally by Lean 4 server.
 -/
-def printPaths (imports : List String := []) : CliM PUnit := do
+def printPaths (imports : List String := []) : CliStateM PUnit := do
   let (lean, lake) ← getInstall
   let configFile := (← getRootDir) / (← getConfigFile)
   if (← configFile.pathExists) then
@@ -239,27 +235,54 @@ def serve (pkg : Package) (args : Array String := #[]) : LakeT IO UInt32 := do
   env (← getLean).toString <| #["--server"] ++ pkg.moreServerArgs ++ args
 
 def command : (cmd : String) → CliM PUnit
-| "new"         => do processOptions; noArgsRem <| new (← takeArg "missing package name")
-| "init"        => do processOptions; noArgsRem <| init (← takeArg "missing package name")
-| "run"         => do processOptions; noArgsRem <| script (← loadPkg) (← takeArg "missing script") (← getSubArgs)
-| "env"         => do exit <| ← withContext <| env (← takeArg "missing command") (← takeArgs).toArray
-| "serve"       => do processOptions; let args ← getSubArgs; exit <| ← noArgsRem <| withPackage fun pkg => serve pkg args.toArray
-| "configure"   => do processOptions; let (ws, pkg) ← loadConfig (← getSubArgs); noArgsRem <| runBuildM ws pkg.buildDepOleans
-| "print-paths" => do processOptions; printPaths (← takeArgs)
-| "build"       => do processOptions; let (ws, pkg) ← loadConfig (← getSubArgs); runBuildM ws <| build pkg (← takeArgs)
-| "clean"       => do processOptions; noArgsRem <| (← loadPkg (← getSubArgs)).clean
-| "self-check"  => do processOptions; noArgsRem <| verifyInstall
-| "help"        => do IO.println <| help (← takeArg?)
-| cmd           => error s!"unknown command '{cmd}'"
+| "new" => do
+  processOptions lakeOption
+  let pkgName ← takeArg "missing package name"
+  noArgsRem <| new pkgName
+| "init" => do
+  processOptions lakeOption
+  let pkgName ← takeArg "missing package name"
+  noArgsRem <| init pkgName
+| "run" => do
+  processOptions lakeOption
+  let scriptName ← takeArg "missing script name"
+  noArgsRem <| script (← loadPkg) scriptName (← getSubArgs)
+| "env" => do
+  let cmd ← takeArg "missing command"; let args ← takeArgs
+  exit <| ← withContext <| env cmd args.toArray
+| "serve" => do
+  let args ← getSubArgs
+  noArgsRem <| exit <| ← withPackage fun pkg => serve pkg args.toArray
+| "configure" => do
+  processOptions lakeOption
+  let (ws, pkg) ← loadConfig (← getSubArgs)
+  noArgsRem <| runBuildM ws pkg.buildDepOleans
+| "print-paths" => do
+  processOptions lakeOption
+  printPaths (← takeArgs)
+| "build" => do
+  processOptions lakeOption
+  let (ws, pkg) ← loadConfig (← getSubArgs)
+  runBuildM ws <| build pkg (← takeArgs)
+| "clean" => do
+  processOptions lakeOption
+  noArgsRem <| (← loadPkg (← getSubArgs)).clean
+| "self-check"  => do
+  processOptions lakeOption
+  noArgsRem <| verifyInstall
+| "help" => do
+  IO.println <| help (← takeArg?)
+| cmd =>
+  error s!"unknown command '{cmd}'"
 
 def processArgs : CliM PUnit := do
   match (← getArgs) with
   | [] => IO.println usage
   | ["--version"] => IO.println uiVersionString
   | _ => -- normal CLI
-    processLeadingOptions -- between `lake` and command
+    processLeadingOptions lakeOption -- between `lake` and command
     if let some cmd ← takeArg? then
-      processLeadingOptions -- between command and args
+      processLeadingOptions lakeOption -- between command and args
       if (← getWantsHelp) then
         IO.println <| help cmd
       else
@@ -272,13 +295,7 @@ end Cli
 open Cli in
 def CliM.run (self : CliM α) (args : List String) : IO UInt32 := do
   let (leanInstall?, lakeInstall?) ← findInstall?
-  let initSt := {leanInstall?, lakeInstall?}
-  let methods := {
-    shortOption,
-    longOption := longOptionOrEq,
-    longShortOption := unknownLongOption,
-  }
-  match (← CliT.run self args methods |>.run' initSt |>.toIO') with
+  match (← self args |>.run' {leanInstall?, lakeInstall?} |>.toIO') with
   | Except.ok _ => pure 0
   | Except.error rc => pure rc
 
diff --git a/Lake/Util/Cli.lean b/Lake/Util/Cli.lean
new file mode 100644
index 0000000000..72ae49c905
--- /dev/null
+++ b/Lake/Util/Cli.lean
@@ -0,0 +1,161 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+
+namespace Lake
+
+/-!
+Defines the abstract CLI interface for Lake.
+-/
+
+-- # Types
+
+def ArgList := List String
+
+@[inline] def ArgList.mk (args : List String) : ArgList :=
+  args
+
+abbrev ArgsT := StateT ArgList
+
+@[inline] def ArgsT.run (args : List String) (self : ArgsT m α) : m (α × List String) :=
+  StateT.run self args
+
+@[inline] def ArgsT.run' [Functor m] (args : List String) (self : ArgsT m α) : m α :=
+  StateT.run' self args
+
+structure OptionHandlers (m : Type u → Type v) (α : Type u) where
+  /-- Process a long option (ex. `--long` or `"--long foo bar"`). -/
+  long : String → m α
+  /-- Process a short option (ex. `-x` or `--`). -/
+  short : Char → m α
+  /-- Process a long short option (ex. `-long`, `-xarg`, `-xyz`). -/
+  longShort : String → m α
+
+-- # Utilities
+
+variable [Monad m] [MonadStateOf ArgList m]
+
+/-- Get the remaining argument list. -/
+@[inline] def getArgs : m (List String) :=
+  get
+
+/-- Replace the argument list. -/
+@[inline] def setArgs (args : List String) : m PUnit :=
+  set (ArgList.mk args)
+
+/-- Take the head of the remaining argument list (or none if empty). -/
+@[inline] def takeArg? : m (Option String) :=
+  modifyGet fun | [] => (none, []) | arg :: args => (some arg, args)
+
+/-- Take the remaining argument list, leaving only an empty list. -/
+@[inline] def takeArgs : m (List String) :=
+  modifyGet fun args => (args, [])
+
+/-- Add a string to the head of the remaining argument list. -/
+@[inline] def consArg (arg : String) : m PUnit :=
+  modify fun args => arg :: args
+
+/-- Process a short option of the form `-x=arg`. -/
+@[inline] def shortOptionWithEq (handle : Char → m α) (opt : String) : m α := do
+  consArg (opt.drop 3); handle opt[1]
+
+/-- Process a short option of the form `"-x arg"`. -/
+@[inline] def shortOptionWithSpace (handle : Char → m α) (opt : String) : m α := do
+  consArg <| opt.drop 2 |>.trimLeft; handle opt[1]
+
+/-- Process a short option of the form `-xarg`. -/
+@[inline] def shortOptionWithArg (handle : Char → m α) (opt : String) : m α := do
+  consArg (opt.drop 2); handle opt[1]
+
+/-- Process a multiple short options grouped together (ex. `-xyz` as `x`, `y`, `z`). -/
+@[inline] def multiShortOption (handle : Char → m PUnit) (opt : String) : m PUnit := do
+  for i in [1:opt.length] do handle opt[i]
+
+/-- Splits a long option of the form `"--long foo bar"` into `--long` and `"foo bar"`. -/
+@[inline] def longOptionOrSpace (handle : String → m α) (opt : String) : m α :=
+  let pos := opt.posOf ' '
+  let arg := opt.drop pos.succ
+  if arg.isEmpty then
+    handle opt
+  else do
+    consArg arg
+    handle <| opt.take pos |>.trimLeft
+
+/-- Splits a long option of the form `--long=arg` into `--long` and `arg`. -/
+@[inline] def longOptionOrEq (handle : String → m α) (opt : String) : m α :=
+  let pos := opt.posOf '='
+  let arg := opt.drop pos.succ
+  if arg.isEmpty then
+    handle opt
+  else do
+    consArg arg
+    handle <| opt.take pos
+
+/-- Process a long option  of the form `--long`, `--long=arg`, `"--long arg"`. -/
+@[inline] def longOption (handle : String → m α) : String → m α :=
+  longOptionOrEq <| longOptionOrSpace handle
+
+/-- Process a short option of the form `-x`, `-x=arg`, `-x arg`, or `-long`. -/
+@[inline] def shortOption
+(shortHandle : Char → m α) (longHandle : String → m α)
+(opt : String) : m α :=
+  if opt.length == 2 then -- `-x`
+    shortHandle opt[1]
+  else -- `-c(.+)`
+    match opt[2] with
+    | '=' => -- `-x=arg`
+      shortOptionWithEq shortHandle opt
+    | ' ' => -- `"-x arg"`
+      shortOptionWithSpace shortHandle opt
+    | _   => -- `-long`
+      longHandle opt
+
+/--
+Process an option, short or long, using the given handlers.
+An option is an argument of length > 1 starting with a dash (`-`).
+An option may consume additional elements of the argument list.
+-/
+@[inline] def option (handlers : OptionHandlers m α) (opt : String) : m α :=
+  if opt[1] == '-' then -- `--(.*)`
+    longOption handlers.long opt
+  else
+    shortOption handlers.short handlers.longShort opt
+
+/-- Process the head argument of the list using `handle` if it is an option. -/
+def processLeadingOption (handle : String → m PUnit) : m PUnit := do
+  match (← getArgs) with
+  | [] => pure ()
+  | arg :: args =>
+    if arg.length > 1 && arg[0] == '-' then -- `-(.+)`
+      setArgs args
+      handle arg
+
+/--
+Process the leading options of the remaining argument list.
+Consumes empty leading arguments in the argument list.
+-/
+partial def processLeadingOptions (handle : String → m PUnit) : m PUnit := do
+  match (← getArgs) with
+  | [] => pure ()
+  | arg :: args =>
+    let len := arg.length
+    if len > 1 && arg[0] == '-' then -- `-(.+)`
+      setArgs args
+      handle arg
+      processLeadingOptions handle
+    else if len == 0 then -- skip empty leading args
+      setArgs args
+      processLeadingOptions handle
+
+/-- Process every option and collect the remaining arguments into an `Array`. -/
+partial def collectArgs (option : String → m PUnit) (args : Array String := #[]) : m (Array String) := do
+  processLeadingOptions option
+  match (← takeArg?) with
+  | some arg => collectArgs option (args.push arg)
+  | none => args
+
+/-- Process every option in the argument list. -/
+@[inline] def processOptions (handle : String → m PUnit) : m PUnit := do
+  setArgs (← collectArgs handle).toList
diff --git a/Lake/Util/CliT.lean b/Lake/Util/CliT.lean
deleted file mode 100644
index 57bf489b93..0000000000
--- a/Lake/Util/CliT.lean
+++ /dev/null
@@ -1,169 +0,0 @@
-/-
-Copyright (c) 2021 Mac Malone. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
--/
-
-namespace Lake
-
---------------------------------------------------------------------------------
--- # CLI Transformer Definition
---------------------------------------------------------------------------------
-
--- Involves trickery patterned after `MacroM`
--- to allow `CliMethods` to refer to `CliT`
-
-constant CliMethodsRefPointed (m : Type → Type v) : PointedType.{0}
-def CliMethodsRef (m : Type → Type v) : Type := (CliMethodsRefPointed m).type
-
-abbrev CliT (m : Type → Type v) :=
-  ReaderT (CliMethodsRef m) <| StateT (List String) m
-
-instance [Pure m] [Inhabited α] : Inhabited (CliT m α) :=
-  ⟨fun _ _ => pure (Inhabited.default, Inhabited.default)⟩
-
-structure CliMethods (m : Type → Type v) where
-  longOption : String → CliT m PUnit
-  longShortOption : String → CliT m PUnit
-  shortOption : Char → CliT m PUnit
-
-instance [Pure m] : Inhabited (CliMethods m) :=
-  ⟨Inhabited.default, Inhabited.default, Inhabited.default⟩
-
-namespace CliMethodsRef
-
-unsafe def mkImp (methods : CliMethods m) : CliMethodsRef m :=
-  unsafeCast methods
-
-@[implementedBy mkImp]
-constant mk (methods : CliMethods m) : CliMethodsRef m :=
-  (CliMethodsRefPointed m).val
-
-instance : Coe (CliMethods m) (CliMethodsRef m) := ⟨mk⟩
-instance [Pure m] : Inhabited (CliMethodsRef m) := ⟨mk Inhabited.default⟩
-
-unsafe def getImp [Pure m] (self : CliMethodsRef m) : CliMethods m :=
-  unsafeCast self
-
-@[implementedBy getImp]
-constant get [Pure m] (self : CliMethodsRef m) : CliMethods m
-
-end CliMethodsRef
-
---------------------------------------------------------------------------------
--- # CLI Utilities
---------------------------------------------------------------------------------
-
-namespace CliT
-variable [Monad m]
-
-/-- Run the CLI on the given argument list using the given methods. -/
-def run (self : CliT m α) (args : List String) (methods : CliMethods m) : m α :=
-  ReaderT.run self methods |>.run' args
-
-/-- Get the remaining argument list. -/
-def getArgs : CliT m (List String) :=
-  get
-
-/-- Replace the argument list. -/
-def setArgs (args : List String) : CliT m PUnit :=
-  set args
-
-/-- Take the head of the remaining argument list (or none if empty). -/
-def takeArg? : CliT m (Option String) :=
-  modifyGet fun | [] => (none, []) | arg :: args => (some arg, args)
-
-/-- Take the remaining argument list, leaving only an empty list. -/
-def takeArgs : CliT m (List String) :=
-  modifyGet fun args => (args, [])
-
-/-- Add a string to the head of the remaining argument list. -/
-def consArg (arg : String) : CliT m PUnit :=
-  modify fun args => arg :: args
-
-/-- Get the methods of this CLI. -/
-def getMethods : CliT m (CliMethods m) :=
-  (·.get) <$> read
-
-/-- Change the methods of this CLI. -/
-def adaptMethods (f : CliMethods m → CliMethods m) (self : CliT m α) : CliT m α :=
-  self.adapt fun ref => CliMethodsRef.mk <| f ref.get
-
-/-- Process a short option (ex. `-x` or `--`). -/
-def shortOption (opt : Char) : CliT m PUnit :=
-  getMethods >>= (·.shortOption opt)
-
-/-- Process a short option of the form `-x=arg`. -/
-def shortOptionEq (opt : String) : CliT m PUnit := do
-  consArg (opt.drop 3); shortOption opt[1]
-
-/-- Process a short option of the form `-xarg`. -/
-def shortOptionArg (opt : String) : CliT m PUnit := do
-  consArg (opt.drop 2); shortOption opt[1]
-
-/-- Process a short option of the form `"-x arg"`. -/
-def shortOptionSpace (opt : String) : CliT m PUnit := do
-  consArg <| opt.drop 2 |>.trimLeft; shortOption opt[1]
-
-/-- Process a multiple short options grouped together (ex. `-xyz` as `x`, `y`, `z`). -/
-def multiShortOption (opt : String) : CliT m PUnit := do
-  for i in [1:opt.length] do shortOption opt[i]
-
-/-- Process a long option (ex. `--long` or `"--long a1 a2"`). -/
-def longOption (opt : String) : CliT m PUnit  := do
-  getMethods >>= (·.longOption opt)
-
-/-- Process a long short option (ex. `-long`, `-xarg`, `-xyz`). -/
-def longShortOption (opt : String) : CliT m PUnit := do
-  getMethods >>= (·.longShortOption opt)
-
-/--
-Process an option, short or long.
-An option is an argument of length > 1 starting with a dash (`-`).
-An option may consume additional elements of the argument list.
--/
-def option (opt : String) : CliT m PUnit :=
-  if opt[1] == '-' then -- `--(.*)`
-    longOption opt
-  else
-    if opt.length == 2 then -- `-x`
-      shortOption opt[1]
-    else -- `-c(.+)`
-      match opt[2] with
-      | '=' => -- `-x=arg`
-        shortOptionEq opt
-      | ' ' => -- `"-x arg"`
-        shortOptionSpace opt
-      | _   => -- `-long`
-        longShortOption opt
-
-/-- Process the leading options of the remaining argument list. -/
-partial def processLeadingOptions : CliT m PUnit := do
-  match (← getArgs) with
-  | [] => pure ()
-  | arg :: args =>
-    let len := arg.length
-    if len > 1 && arg[0] == '-' then -- `-(.+)`
-      setArgs args
-      option arg
-      processLeadingOptions
-    else if len == 0 then -- skip empty leading args
-      setArgs args
-      processLeadingOptions
-
-/-- Process every option and collect the remaining arguments into the given `Array`. -/
-partial def collectArgsInto (arr : Array String) : CliT m (Array String) := do
-  processLeadingOptions
-  match (← takeArg?) with
-  | some arg => collectArgsInto (arr.push arg)
-  | none => arr
-
-/-- Process every option and collect the remaining arguments into an `Array`. -/
-def collectArgs : CliT m (Array String) :=
-  collectArgsInto #[]
-
-/-- Process every option in the argument list. -/
-def processOptions : CliT m PUnit := do
-  setArgs (← collectArgs).toList
-
-end CliT