diff --git a/Cli.lean b/Cli.lean
index ec8c71e..44206f4 100644
--- a/Cli.lean
+++ b/Cli.lean
@@ -1,4 +1,5 @@
 module
 
 public import Cli.Basic
-public import Cli.Extensions
\ No newline at end of file
+public import Cli.Extensions
+public import Cli.Typed
\ No newline at end of file
diff --git a/Cli/Basic.lean b/Cli/Basic.lean
index 2b1e254..a350f63 100644
--- a/Cli/Basic.lean
+++ b/Cli/Basic.lean
@@ -1018,17 +1018,20 @@ section Macro
       ("EXTENSIONS: " sepBy(term, ";", "; "))?
     "\n]" : term
 
-  meta def expandNameableStringArg (t : TSyntax `Cli.nameableStringArg) : MacroM Term :=
+  meta def expandNameableStringArg (t : TSyntax ``Cli.nameableStringArg) : MacroM Term :=
     pure ⟨t.raw[0]⟩
 
-  meta def expandLiteralIdent (t : TSyntax `Cli.literalIdent) : MacroM Term :=
+  meta def extractLiteralIdent (t : TSyntax ``Cli.literalIdent) : String :=
     let s := t.raw[0]
     if s.getKind == identKind then
-      pure <| quote s.getId.toString
+      s.getId.toString
     else
-      pure ⟨s⟩
+      s.isStrLit?.get!
 
-  meta def expandRunFun (runFun : TSyntax `Cli.runFun) : MacroM Term :=
+  meta def expandLiteralIdent (t : TSyntax ``Cli.literalIdent) : MacroM Term :=
+    pure <| quote <| extractLiteralIdent t
+
+  meta def expandRunFun (runFun : TSyntax ``Cli.runFun) : MacroM Term :=
     match runFun with
     | `(Cli.runFun| VIA $run) =>
       `($run)
@@ -1036,17 +1039,17 @@ section Macro
       `(fun _ => pure 0)
     | _ => Macro.throwUnsupported
 
-  meta def expandPositionalArg (positionalArg : TSyntax `Cli.positionalArg) : MacroM Term := do
+  meta def expandPositionalArg (positionalArg : TSyntax ``Cli.positionalArg) : MacroM Term := do
     let `(Cli.positionalArg| $name : $type; $description) := positionalArg
       | Macro.throwUnsupported
     `(Arg.mk $(← expandLiteralIdent name) $(← expandNameableStringArg description) $type)
 
-  meta def expandVariableArg (variableArg : TSyntax `Cli.variableArg) : MacroM Term := do
+  meta def expandVariableArg (variableArg : TSyntax ``Cli.variableArg) : MacroM Term := do
     let `(Cli.variableArg| ...$name : $type; $description) := variableArg
       | Macro.throwUnsupported
     `(Arg.mk $(← expandLiteralIdent name) $(← expandNameableStringArg description) $type)
 
-  meta def expandFlag (flag : TSyntax `Cli.flag) : MacroM Term := do
+  meta def expandFlag (flag : TSyntax ``Cli.flag) : MacroM Term := do
     let `(Cli.flag| $flagName1 $[, $flagName2]? $[ : $type]?; $description) := flag
       | Macro.throwUnsupported
     let mut shortName := quote (none : Option String)
@@ -1061,31 +1064,53 @@ section Macro
       | some type => type
     `(Flag.mk $shortName $(← expandLiteralIdent longName) $(← expandNameableStringArg description) $type)
 
+  meta def mkCmdInstantiationTerm
+      (name : TSyntax ``Cli.literalIdent)
+      (version? : Option (TSyntax ``Cli.nameableStringArg))
+      (description : TSyntax ``Cli.nameableStringArg)
+      (flags? : Option (TSyntaxArray ``Cli.flag))
+      (positionalArgs? : Option (TSyntaxArray ``Cli.positionalArg))
+      (variableArg? : Option (Option (TSyntax ``Cli.variableArg)))
+      (subCommands? : Option (Lean.Syntax.TSepArray `ident ";"))
+      (extensions? : Option (Lean.Syntax.TSepArray `term ";"))
+      (run : Term)
+      : MacroM Term := do
+    `(Cmd.mk
+        (name           := $(← expandLiteralIdent name))
+        (version?       := $(quote (← version?.mapM expandNameableStringArg)))
+        (description    := $(← expandNameableStringArg description))
+        (flags          := $(quote (← flags?.getD #[] |>.mapM expandFlag)))
+        (positionalArgs := $(quote (← positionalArgs?.getD #[] |>.mapM expandPositionalArg)))
+        (variableArg?   := $(quote (← (Option.join variableArg?).mapM expandVariableArg)))
+        (run            := $run)
+        (subCmds        := $(quote ((subCommands?.getD ⟨#[]⟩).getElems : TSyntaxArray `term)))
+        (extension?     := some <| Array.foldl Extension.then { : Extension } <| Array.qsort
+          $(quote (extensions?.getD ⟨#[]⟩).getElems) (·.priority > ·.priority)))
+
   macro_rules
     | `(`[Cli|
         $name $run:runFun; $[[$version?]]?
         $description
         $[FLAGS:
-          $flags*
+          $flags?*
         ]?
         $[ARGS:
-          $positionalArgs*
-          $[$variableArg]?
+          $positionalArgs?*
+          $[$variableArg?]?
         ]?
-        $[SUBCOMMANDS: $subCommands;*]?
-        $[EXTENSIONS: $extensions;*]?
+        $[SUBCOMMANDS: $subCommands?;*]?
+        $[EXTENSIONS: $extensions?;*]?
       ]) => do
-        `(Cmd.mk
-          (name           := $(← expandLiteralIdent name))
-          (version?       := $(quote (← version?.mapM expandNameableStringArg)))
-          (description    := $(← expandNameableStringArg description))
-          (flags          := $(quote (← flags.getD #[] |>.mapM expandFlag)))
-          (positionalArgs := $(quote (← positionalArgs.getD #[] |>.mapM expandPositionalArg)))
-          (variableArg?   := $(quote (← (Option.join variableArg).mapM expandVariableArg)))
-          (run            := $(← expandRunFun run))
-          (subCmds        := $(quote ((subCommands.getD ⟨#[]⟩).getElems : TSyntaxArray `term)))
-          (extension?     := some <| Array.foldl Extension.then { : Extension } <| Array.qsort
-            $(quote (extensions.getD ⟨#[]⟩).getElems) (·.priority > ·.priority)))
+        mkCmdInstantiationTerm
+          name
+          version?
+          description
+          flags?
+          positionalArgs?
+          variableArg?
+          subCommands?
+          extensions?
+          (← expandRunFun run)
 end Macro
 
 section Info
diff --git a/Cli/Typed.lean b/Cli/Typed.lean
new file mode 100644
index 0000000..0f184b9
--- /dev/null
+++ b/Cli/Typed.lean
@@ -0,0 +1,184 @@
+module
+
+public import Cli.Basic
+meta import Init.Data.Slice.Array.Iterator
+meta import Init.Data.Slice.Array.Basic
+
+section
+
+namespace Cli
+
+open Lean
+
+section TypedCli
+  private meta def kebabToCamelCase (s : String) : String := Id.run do
+    let parts := s.split "-" |>.toArray
+    let mut result : String := parts[0]!.toString
+    for part in parts[1...*] do
+      let some frontChar := part.front?
+        | continue
+      let frontChar := frontChar.toUpper
+      let rest := part.drop 1
+      result := result.push frontChar ++ rest
+    return result
+
+  private meta def mkTypedParsedDecls
+      (name : TSyntax ``Cli.literalIdent)
+      (version? : Option (TSyntax ``Cli.nameableStringArg))
+      (description : TSyntax ``Cli.nameableStringArg)
+      (flags? : Option (TSyntaxArray ``Cli.flag))
+      (positionalArgs? : Option (TSyntaxArray ``Cli.positionalArg))
+      (variableArg? : Option (Option (TSyntax ``Cli.variableArg)))
+      (subCommands? : Option (Lean.Syntax.TSepArray `ident ";"))
+      (extensions? : Option (Lean.Syntax.TSepArray `term ";"))
+      : MacroM (Array Syntax) := do
+    let cmdName := .mkSimple <| extractLiteralIdent name
+    let cmdConstructorIdent := mkIdent (.str cmdName "mkCmd")
+    let typedParsedDeclName := .str cmdName "Parsed"
+    let typedParsedDeclIdent := mkIdent typedParsedDeclName
+    let typedParsedDeclRawConstructorIdent := mkIdent (.str typedParsedDeclName "mk")
+
+    let typedParsedDecl ← `(
+      structure $typedParsedDeclIdent where
+        raw : Cli.Parsed
+      deriving Inhabited
+    )
+
+    let mut typedParsedDeclAccessors : Array Syntax := #[]
+    for flag in flags?.getD #[] do
+      let `(Cli.flag| $flagName1 $[, $flagName2?]? $[ : $flagType?]?; $_) := flag
+        | Macro.throwUnsupported
+      let longFlagName := extractLiteralIdent <| flagName2?.getD flagName1
+      let longFlagNameTerm := quote longFlagName
+      let flagAccessorName := kebabToCamelCase longFlagName
+      let flagAccessor ←
+        match flagType? with
+        | none =>
+          let flagAccessorIdent := mkIdent (.str typedParsedDeclName flagAccessorName)
+          `(
+            @[inline] def $flagAccessorIdent (p : $typedParsedDeclIdent) : Bool :=
+              p.raw.hasFlag $longFlagNameTerm
+          )
+        | some flagType =>
+          let flagAccessorIdent := mkIdent (.str typedParsedDeclName (flagAccessorName ++ "?"))
+          `(
+            @[inline] def $flagAccessorIdent (p : $typedParsedDeclIdent) : Option $flagType :=
+              p.raw.flag? $longFlagNameTerm |>.map (·.as! $flagType)
+          )
+      typedParsedDeclAccessors := typedParsedDeclAccessors.push flagAccessor
+    for arg in positionalArgs?.getD #[] do
+      let `(Cli.positionalArg| $argName : $argType; $_) := arg
+        | Macro.throwUnsupported
+      let argName := extractLiteralIdent argName
+      let argNameTerm := quote argName
+      let argAccessorName := kebabToCamelCase argName
+      let argAccessorIdent := mkIdent (.str typedParsedDeclName argAccessorName)
+      let argAccessor ← `(
+        @[inline] def $argAccessorIdent (p : $typedParsedDeclIdent) : $argType :=
+          p.raw.positionalArg! $argNameTerm |>.as! $argType
+      )
+      typedParsedDeclAccessors := typedParsedDeclAccessors.push argAccessor
+    if let some variableArg := Option.join variableArg? then
+      let `(Cli.variableArg| ...$variableArgName : $variableArgType; $_) := variableArg
+        | Macro.throwUnsupported
+      let variableArgAccessorName := extractLiteralIdent variableArgName |> kebabToCamelCase
+      let variableArgAccessorIdent := mkIdent (.str typedParsedDeclName variableArgAccessorName)
+      let variableArgAccessor ← `(
+        @[inline] def $variableArgAccessorIdent (p : $typedParsedDeclIdent) : Array $variableArgType :=
+          p.raw.variableArgsAs! $variableArgType
+      )
+      typedParsedDeclAccessors := typedParsedDeclAccessors.push variableArgAccessor
+
+    let cmdInstantiationTerm ← mkCmdInstantiationTerm
+      name
+      version?
+      description
+      flags?
+      positionalArgs?
+      variableArg?
+      subCommands?
+      extensions?
+      (← `(fun raw => handler ($typedParsedDeclRawConstructorIdent raw)))
+    let cmdConstructor ← `(
+      def $cmdConstructorIdent
+          (handler : $typedParsedDeclIdent → IO UInt32)
+          : Cmd :=
+        $cmdInstantiationTerm
+    )
+
+    return #[typedParsedDecl] ++ typedParsedDeclAccessors ++ #[cmdConstructor]
+
+  syntax "cli_def " literalIdent runFun "; " ("[" nameableStringArg "]")?
+      nameableStringArg
+      ("FLAGS:\n" withPosition((flag)*))?
+      ("ARGS:\n" withPosition((positionalArg)* (variableArg)?))?
+      ("SUBCOMMANDS: " sepBy(ident, ";", "; "))?
+      ("EXTENSIONS: " sepBy(term, ";", "; "))?
+    : command
+
+  syntax "cli_def " literalIdent "; " ("[" nameableStringArg "]")?
+      nameableStringArg
+      ("FLAGS:\n" withPosition((flag)*))?
+      ("ARGS:\n" withPosition((positionalArg)* (variableArg)?))?
+      ("SUBCOMMANDS: " sepBy(ident, ";", "; "))?
+      ("EXTENSIONS: " sepBy(term, ";", "; "))?
+      (" RUN " term)?
+    : command
+
+  macro_rules
+    | `(cli_def $name $run:runFun; $[[$version?]]?
+        $description
+        $[FLAGS:
+          $flags?*
+        ]?
+        $[ARGS:
+          $positionalArgs?*
+          $[$variableArg?]?
+        ]?
+        $[SUBCOMMANDS: $subCommands?;*]?
+        $[EXTENSIONS: $extensions?;*]? ) => do
+      let cmdIdent := mkIdent (.mkSimple (extractLiteralIdent name))
+      let cmdMk ← mkCmdInstantiationTerm
+        name
+        version?
+        description
+        flags?
+        positionalArgs?
+        variableArg?
+        subCommands?
+        extensions?
+        (← expandRunFun run)
+      `(def $cmdIdent : Cmd := $cmdMk)
+
+  macro_rules
+    | `(cli_def $name; $[[$version?]]?
+        $description
+        $[FLAGS:
+          $flags?*
+        ]?
+        $[ARGS:
+          $positionalArgs?*
+          $[$variableArg?]?
+        ]?
+        $[SUBCOMMANDS: $subCommands?;*]?
+        $[EXTENSIONS: $extensions?;*]?
+        $[RUN $handlerTerm?]?) => do
+      let typedParsedDecls ← mkTypedParsedDecls
+        name
+        version?
+        description
+        flags?
+        positionalArgs?
+        variableArg?
+        subCommands?
+        extensions?
+      let some handlerTerm := handlerTerm?
+        | return mkNullNode typedParsedDecls
+      let cmdName := .mkSimple <| extractLiteralIdent name
+      let cmdIdent := mkIdent cmdName
+      let cmdConstructorIdent := mkIdent (Name.mkStr cmdName "mkCmd")
+      let cmd ← `(def $cmdIdent : Cmd := $cmdConstructorIdent $handlerTerm)
+      return mkNullNode (typedParsedDecls ++ #[cmd])
+end TypedCli
+
+end Cli
diff --git a/CliTest/Example.lean b/CliTest/Example.lean
index af86a39..4b69977 100644
--- a/CliTest/Example.lean
+++ b/CliTest/Example.lean
@@ -2,43 +2,14 @@ import Cli
 
 open Cli
 
-def runExampleCmd (p : Parsed) : IO UInt32 := do
-  let input   : String       := p.positionalArg! "input" |>.as! String
-  let outputs : Array String := p.variableArgsAs! String
-  IO.println <| "Input: " ++ input
-  IO.println <| "Outputs: " ++ toString outputs
-
-  if p.hasFlag "verbose" then
-    IO.println "Flag `--verbose` was set."
-  if p.hasFlag "invert" then
-    IO.println "Flag `--invert` was set."
-  if p.hasFlag "optimize" then
-    IO.println "Flag `--optimize` was set."
-
-  let priority : Nat := p.flag! "priority" |>.as! Nat
-  IO.println <| "Flag `--priority` always has at least a default value: " ++ toString priority
-
-  if p.hasFlag "module" then
-    let moduleName : ModuleName := p.flag! "module" |>.as! ModuleName
-    IO.println <| s!"Flag `--module` was set to `{moduleName}`."
-
-  if let some setPathsFlag := p.flag? "set-paths" then
-    IO.println <| toString <| setPathsFlag.as! (Array String)
-  return 0
-
-def installCmd := `[Cli|
-  installCmd NOOP;
+cli_def installCmd NOOP;
   "installCmd provides an example for a subcommand without flags or arguments that does nothing. \
    Versions can be omitted."
-]
 
-def testCmd := `[Cli|
-  testCmd NOOP;
+cli_def testCmd NOOP;
   "testCmd provides another example for a subcommand without flags or arguments that does nothing."
-]
 
-def exampleCmd : Cmd := `[Cli|
-  exampleCmd VIA runExampleCmd; ["0.0.1"]
+cli_def exampleCmd; ["0.0.1"]
   "This string denotes the description of `exampleCmd`."
 
   FLAGS:
@@ -51,7 +22,7 @@ def exampleCmd : Cmd := `[Cli|
                                  which can be used to reference Lean modules like `Init.Data.Array` \
                                  or Lean files using a relative path like `Init/Data/Array.lean`."
     "set-paths" : Array String; "Declares a flag `--set-paths` \
-                                 that takes an argument of type `Array Nat`. \
+                                 that takes an argument of type `Array String`. \
                                  Quotation marks allow the use of hyphens."
 
   ARGS:
@@ -70,7 +41,30 @@ def exampleCmd : Cmd := `[Cli|
   EXTENSIONS:
     author "mhuisi";
     defaultValues! #[("priority", "0")]
-]
+
+def runExampleCmd (p : exampleCmd.Parsed) : IO UInt32 := do
+  IO.println <| "Input: " ++ p.input
+  IO.println <| "Outputs: " ++ toString p.outputs
+
+  if p.verbose then
+    IO.println "Flag `--verbose` was set."
+  if p.invert then
+    IO.println "Flag `--invert` was set."
+  if p.optimize then
+    IO.println "Flag `--optimize` was set."
+
+  let priority : Nat := p.priority?.getD 0
+  IO.println <| "Flag `--priority` always has at least a default value: " ++ toString priority
+
+  if let some moduleName := p.module? then
+    IO.println <| s!"Flag `--module` was set to `{moduleName}`."
+
+  if let some setPaths := p.setPaths? then
+    IO.println <| toString setPaths
+
+  return 0
+
+def exampleCmd : Cmd := exampleCmd.mkCmd runExampleCmd
 
 def main (args : List String) : IO UInt32 :=
   exampleCmd.validate args
@@ -106,7 +100,6 @@ Yields:
   0.0.1
 -/
 
-
 #eval main <| "-h".splitOn " "
 /-
 Yields:
@@ -135,7 +128,7 @@ Yields:
                                   or Lean files using a relative path like
                                   `Init/Data/Array.lean`.
       --set-paths : Array String  Declares a flag `--set-paths` that takes an
-                                  argument of type `Array Nat`. Quotation marks
+                                  argument of type `Array String`. Quotation marks
                                   allow the use of hyphens.
 
   ARGS:
diff --git a/CliTest/Tests.lean b/CliTest/Tests.lean
index bfd41f0..cc1c020 100644
--- a/CliTest/Tests.lean
+++ b/CliTest/Tests.lean
@@ -1,5 +1,6 @@
 import Cli.Basic
 import Cli.Extensions
+import Cli.Typed
 
 namespace Cli
 
@@ -416,4 +417,503 @@ end InvalidInputs
 
 end ModuleName
 
+section CliDef
+
+-- Test cli_def VIA (backward-compatible mode)
+cli_def viaSubCmd VIA doNothing;
+  "a subcommand defined with cli_def VIA"
+
+-- Test cli_def NOOP
+cli_def noopSubCmd NOOP;
+  "a subcommand defined with cli_def NOOP"
+
+-- Test cli_def VIA with flags, args, extensions
+cli_def viaCmd VIA doNothing; ["1.0.0"]
+  "a command defined with cli_def VIA"
+
+  FLAGS:
+    verbose; "verbose flag"
+    n, count : Nat; "a typed flag"
+
+  ARGS:
+    input : String; "an input"
+
+  SUBCOMMANDS: viaSubCmd; noopSubCmd
+
+  EXTENSIONS:
+    defaultValues! #[("count", "0")]
+
+section ViaValidInputs
+
+/--
+info: "cmd: viaCmd; flags: #[--count=0]; positionalArgs: #[<input=hello>]; variableArgs: #[]"
+-/
+#guard_msgs in
+#eval viaCmd.processParsed "hello"
+
+/--
+info: "cmd: viaCmd; flags: #[--verbose, --count=5]; positionalArgs: #[<input=hello>]; variableArgs: #[]"
+-/
+#guard_msgs in
+#eval viaCmd.processParsed "--verbose -n5 hello"
+
+/--
+info: "cmd: viaCmd noopSubCmd; flags: #[]; positionalArgs: #[]; variableArgs: #[]"
+-/
+#guard_msgs in
+#eval viaCmd.processParsed "noopSubCmd"
+
+end ViaValidInputs
+
+section ViaInvalidInputs
+
+/-- info: "Missing positional argument `<input>.`" -/
+#guard_msgs in
+#eval viaCmd.processParsed ""
+
+end ViaInvalidInputs
+
+-- Test cli_def RUN: typed struct generation and accessor correctness
+
+-- A simple subcommand used by the typed command
+cli_def typedSubCmd NOOP;
+  "a subcommand for the typed command"
+
+-- The main typed command exercises all feature combinations:
+-- parameterless flags, typed flags, short aliases, hyphenated names,
+-- positional args, variable args, subcommands, and extensions.
+cli_def typedCmd; ["2.0.0"]
+  "a command defined with cli_def RUN"
+
+  FLAGS:
+    verbose;                     "verbose flag"
+    x, unknown1;                 "flag with short name"
+    t, typed1 : String;          "typed flag"
+    "p-n", "level-param" : Nat;  "hyphenated flag"
+
+  ARGS:
+    input1 : String;     "a string input"
+    input2 : Array Nat;  "an array input"
+    ...outputs : Nat;    "varargs"
+
+  SUBCOMMANDS: typedSubCmd
+
+  EXTENSIONS:
+    defaultValues! #[("level-param", "0")]
+
+  RUN fun p => do
+    -- Exercise every accessor to verify types are correct
+    IO.println <| "input1=" ++ p.input1
+    IO.println <| "input2=" ++ toString p.input2
+    IO.println <| "outputs=" ++ toString p.outputs
+    IO.println <| "verbose=" ++ toString p.verbose
+    IO.println <| "unknown1=" ++ toString p.unknown1
+    IO.println <| "typed1=" ++ toString p.typed1?
+    IO.println <| "levelParam=" ++ toString p.levelParam?
+    return 0
+
+section TypedStructExists
+
+-- Verify the Parsed struct exists and is Inhabited
+#check typedCmd.Parsed
+#check (inferInstance : Inhabited typedCmd.Parsed)
+
+-- Verify accessor types
+#check @typedCmd.Parsed.verbose   -- typedCmd.Parsed → Bool
+#check @typedCmd.Parsed.unknown1  -- typedCmd.Parsed → Bool
+#check @typedCmd.Parsed.typed1?    -- typedCmd.Parsed → Option String
+#check @typedCmd.Parsed.levelParam? -- typedCmd.Parsed → Option Nat
+#check @typedCmd.Parsed.input1    -- typedCmd.Parsed → String
+#check @typedCmd.Parsed.input2    -- typedCmd.Parsed → Array Nat
+#check @typedCmd.Parsed.outputs   -- typedCmd.Parsed → Array Nat
+#check @typedCmd.Parsed.raw       -- typedCmd.Parsed → Cli.Parsed
+
+end TypedStructExists
+
+section TypedValidInputs
+
+/--
+info: input1=foo
+input2=#[1, 2, 3]
+outputs=#[4, 5]
+verbose=true
+unknown1=false
+typed1=(some hello)
+levelParam=(some 7)
+---
+info: 0
+-/
+#guard_msgs in
+#eval typedCmd.validate <| "--verbose -t hello --level-param=7 foo 1,2,3 4 5".splitOn " "
+
+/--
+info: input1=foo
+input2=#[1]
+outputs=#[]
+verbose=false
+unknown1=true
+typed1=(some bar)
+levelParam=(some 0)
+---
+info: 0
+-/
+#guard_msgs in
+#eval typedCmd.validate <| "-x -tbar foo 1".splitOn " "
+
+/--
+info: input1=foo
+input2=#[1]
+outputs=#[]
+verbose=false
+unknown1=false
+typed1=none
+levelParam=(some 0)
+---
+info: 0
+-/
+#guard_msgs in
+#eval typedCmd.validate <| "foo 1".splitOn " "
+
+end TypedValidInputs
+
+section TypedParsing
+
+-- Verify that the typed command produces the same parse results as a
+-- manually-defined equivalent using `[Cli| ...]`
+def typedCmdEquiv : Cmd := `[Cli|
+  typedCmd VIA doNothing; ["2.0.0"]
+  "a command defined with cli_def RUN"
+
+  FLAGS:
+    verbose;                     "verbose flag"
+    x, unknown1;                 "flag with short name"
+    t, typed1 : String;          "typed flag"
+    "p-n", "level-param" : Nat;  "hyphenated flag"
+
+  ARGS:
+    input1 : String;     "a string input"
+    input2 : Array Nat;  "an array input"
+    ...outputs : Nat;    "varargs"
+
+  SUBCOMMANDS: typedSubCmd
+
+  EXTENSIONS:
+    defaultValues! #[("level-param", "0")]
+]
+
+/--
+info: "cmd: typedCmd; flags: #[--verbose, --typed1=hello, --level-param=0]; positionalArgs: #[<input1=foo>, <input2=1,2,3>]; variableArgs: #[<outputs=4>, <outputs=5>]"
+-/
+#guard_msgs in
+#eval typedCmd.processParsed "--verbose -t hello foo 1,2,3 4 5"
+
+-- Same parse result from the equivalent command
+/--
+info: "cmd: typedCmd; flags: #[--verbose, --typed1=hello, --level-param=0]; positionalArgs: #[<input1=foo>, <input2=1,2,3>]; variableArgs: #[<outputs=4>, <outputs=5>]"
+-/
+#guard_msgs in
+#eval typedCmdEquiv.processParsed "--verbose -t hello foo 1,2,3 4 5"
+
+end TypedParsing
+
+section TypedInvalidInputs
+
+/-- info: "Missing positional argument `<input1>.`" -/
+#guard_msgs in
+#eval typedCmd.processParsed ""
+
+/-- info: "Missing positional argument `<input2>.`" -/
+#guard_msgs in
+#eval typedCmd.processParsed "foo"
+
+/-- info: "Invalid type of argument `abc` for positional argument `<input2 : Array Nat>`." -/
+#guard_msgs in
+#eval typedCmd.processParsed "foo abc"
+
+/-- info: "Unknown flag `--nonexistent`." -/
+#guard_msgs in
+#eval typedCmd.processParsed "foo 1 --nonexistent"
+
+end TypedInvalidInputs
+
+section TypedInfo
+
+/--
+info: "typedCmd [2.0.0]\na command defined with cli_def RUN\n\nUSAGE:\n    typedCmd [SUBCOMMAND] [FLAGS] <input1> <input2> <outputs>...\n\nFLAGS:\n    -h, --help                 Prints this message.\n    --version                  Prints the version.\n    --verbose                  verbose flag\n    -x, --unknown1             flag with short name\n    -t, --typed1 : String      typed flag\n    -p-n, --level-param : Nat  hyphenated flag [Default: `0`]\n\nARGS:\n    input1 : String     a string input\n    input2 : Array Nat  an array input\n    outputs : Nat       varargs\n\nSUBCOMMANDS:\n    typedSubCmd  a subcommand for the typed command"
+-/
+#guard_msgs in
+#eval typedCmd.extendedHelp
+
+end TypedInfo
+
+-- Test: cli_def RUN with no flags and no variable args
+cli_def minimalCmd;
+  "a minimal command with only a positional arg"
+
+  ARGS:
+    name : String; "your name"
+
+  RUN fun p => do
+    IO.println <| "Hello, " ++ p.name
+    return 0
+
+/--
+info: Hello, World
+---
+info: 0
+-/
+#guard_msgs in
+#eval minimalCmd.validate <| ["World"]
+
+-- Test: cli_def RUN with only flags, no args
+cli_def flagsOnlyCmd;
+  "a command with only flags"
+
+  FLAGS:
+    a, alpha; "first flag"
+    b, beta;  "second flag"
+
+  RUN fun p => do
+    IO.println <| "alpha=" ++ toString p.alpha ++ " beta=" ++ toString p.beta
+    return 0
+
+/--
+info: alpha=true beta=false
+---
+info: 0
+-/
+#guard_msgs in
+#eval flagsOnlyCmd.validate <| ["-a"]
+
+/--
+info: alpha=true beta=true
+---
+info: 0
+-/
+#guard_msgs in
+#eval flagsOnlyCmd.validate <| ["-ab"]
+
+-- Test: hyphenToCamelCase conversion for hyphenated arg names
+cli_def hyphenCmd;
+  "tests hyphenated names"
+
+  FLAGS:
+    "my-flag"; "a hyphenated flag"
+    "another-long-flag" : String; "a typed hyphenated flag"
+
+  ARGS:
+    "my-input" : String; "a hyphenated arg"
+
+  RUN fun p => do
+    IO.println <| "myFlag=" ++ toString p.myFlag
+    IO.println <| "anotherLongFlag=" ++ toString p.anotherLongFlag?
+    IO.println <| "myInput=" ++ p.myInput
+    return 0
+
+/--
+info: myFlag=true
+anotherLongFlag=(some hello)
+myInput=world
+---
+info: 0
+-/
+#guard_msgs in
+#eval hyphenCmd.validate <| "--my-flag --another-long-flag=hello world".splitOn " "
+
+-- Test: raw accessor provides access to underlying Cli.Parsed
+cli_def rawAccessCmd;
+  "tests raw accessor"
+
+  ARGS:
+    input : String; "an input"
+
+  RUN fun p => do
+    -- Access via typed accessor
+    IO.println <| "typed: " ++ p.input
+    -- Access via raw Cli.Parsed
+    IO.println <| "raw: " ++ (p.raw.positionalArg! "input" |>.as! String)
+    return 0
+
+/--
+info: typed: hello
+raw: hello
+---
+info: 0
+-/
+#guard_msgs in
+#eval rawAccessCmd.validate <| ["hello"]
+
+-- Test: signature-only cli_def generates struct + mkCmd but no `def`
+cli_def sigOnlyCmd; ["1.0.0"]
+  "a command defined with signature-only cli_def"
+
+  FLAGS:
+    verbose;             "verbose flag"
+    n, count : Nat;      "a count flag"
+
+  ARGS:
+    input : String;      "an input"
+    ...extras : String;  "extra args"
+
+section SigOnlyStructExists
+-- Verify the struct and mkCmd exist
+#check sigOnlyCmd.Parsed
+#check (inferInstance : Inhabited sigOnlyCmd.Parsed)
+#check @sigOnlyCmd.Parsed.verbose  -- sigOnlyCmd.Parsed → Bool
+#check @sigOnlyCmd.Parsed.count?    -- sigOnlyCmd.Parsed → Option Nat
+#check @sigOnlyCmd.Parsed.input    -- sigOnlyCmd.Parsed → String
+#check @sigOnlyCmd.Parsed.extras   -- sigOnlyCmd.Parsed → Array String
+#check @sigOnlyCmd.mkCmd           -- (sigOnlyCmd.Parsed → IO UInt32) → Cmd
+end SigOnlyStructExists
+
+-- Define the handler as a standalone function using the generated type
+def runSigOnlyCmd (p : sigOnlyCmd.Parsed) : IO UInt32 := do
+  IO.println <| "input=" ++ p.input
+  IO.println <| "extras=" ++ toString p.extras
+  IO.println <| "verbose=" ++ toString p.verbose
+  IO.println <| "count=" ++ toString p.count?
+  return 0
+
+-- Attach the handler via mkCmd
+def sigOnlyCmd : Cmd := sigOnlyCmd.mkCmd runSigOnlyCmd
+
+/--
+info: input=hello
+extras=#[a, b]
+verbose=true
+count=(some 42)
+---
+info: 0
+-/
+#guard_msgs in
+#eval sigOnlyCmd.validate <| "--verbose --count=42 hello a b".splitOn " "
+
+/--
+info: input=world
+extras=#[]
+verbose=false
+count=none
+---
+info: 0
+-/
+#guard_msgs in
+#eval sigOnlyCmd.validate <| ["world"]
+
+-- Verify help output includes all metadata
+/--
+info: "sigOnlyCmd [1.0.0]\na command defined with signature-only cli_def\n\nUSAGE:\n    sigOnlyCmd [FLAGS] <input> <extras>...\n\nFLAGS:\n    -h, --help         Prints this message.\n    --version          Prints the version.\n    --verbose          verbose flag\n    -n, --count : Nat  a count flag\n\nARGS:\n    input : String   an input\n    extras : String  extra args"
+-/
+#guard_msgs in
+#eval sigOnlyCmd.extendedHelp
+
+-- Test: signature-only with RUN-equivalent pattern produces same results
+-- as inline RUN
+cli_def sigEquivCmd;
+  "equivalent command"
+
+  FLAGS:
+    verbose; "verbose"
+
+  ARGS:
+    name : String; "a name"
+
+  RUN fun p => do
+    IO.println <| "name=" ++ p.name ++ " verbose=" ++ toString p.verbose
+    return 0
+
+cli_def sigEquivCmd2;
+  "equivalent command"
+
+  FLAGS:
+    verbose; "verbose"
+
+  ARGS:
+    name : String; "a name"
+
+def sigEquivCmd2 : Cmd := sigEquivCmd2.mkCmd fun p => do
+  IO.println <| "name=" ++ p.name ++ " verbose=" ++ toString p.verbose
+  return 0
+
+-- Both should produce the same output
+/--
+info: name=Alice verbose=true
+---
+info: 0
+-/
+#guard_msgs in
+#eval sigEquivCmd.validate <| "--verbose Alice".splitOn " "
+
+/--
+info: name=Alice verbose=true
+---
+info: 0
+-/
+#guard_msgs in
+#eval sigEquivCmd2.validate <| "--verbose Alice".splitOn " "
+
+-- Test: signature-only cli_def with subcommands
+cli_def sigSubA NOOP;
+  "subcommand A"
+
+cli_def sigSubB;
+  "subcommand B"
+
+  FLAGS:
+    force; "force flag"
+
+  RUN fun p => do
+    IO.println <| "subB force=" ++ toString p.force
+    return 0
+
+cli_def sigParentCmd; ["3.0.0"]
+  "a parent command with subcommands, defined signature-only"
+
+  FLAGS:
+    verbose; "verbose flag"
+
+  ARGS:
+    target : String; "a target"
+
+  SUBCOMMANDS:
+    sigSubA;
+    sigSubB
+
+def runSigParentCmd (p : sigParentCmd.Parsed) : IO UInt32 := do
+  IO.println <| "target=" ++ p.target ++ " verbose=" ++ toString p.verbose
+  return 0
+
+def sigParentCmd : Cmd := sigParentCmd.mkCmd runSigParentCmd
+
+-- Run parent command
+/--
+info: target=foo verbose=true
+---
+info: 0
+-/
+#guard_msgs in
+#eval sigParentCmd.validate <| "--verbose foo".splitOn " "
+
+-- Run subcommand A (NOOP)
+/-- info: 0 -/
+#guard_msgs in
+#eval sigParentCmd.validate <| "sigSubA".splitOn " "
+
+-- Run subcommand B
+/--
+info: subB force=true
+---
+info: 0
+-/
+#guard_msgs in
+#eval sigParentCmd.validate <| "sigSubB --force".splitOn " "
+
+-- Verify help lists subcommands
+/--
+info: "sigParentCmd [3.0.0]\na parent command with subcommands, defined signature-only\n\nUSAGE:\n    sigParentCmd [SUBCOMMAND] [FLAGS] <target>\n\nFLAGS:\n    -h, --help  Prints this message.\n    --version   Prints the version.\n    --verbose   verbose flag\n\nARGS:\n    target : String  a target\n\nSUBCOMMANDS:\n    sigSubA  subcommand A\n    sigSubB  subcommand B"
+-/
+#guard_msgs in
+#eval sigParentCmd.extendedHelp
+
+end CliDef
+
 end Cli
diff --git a/README.md b/README.md
index 099320f..2fef019 100644
--- a/README.md
+++ b/README.md
@@ -5,24 +5,21 @@ This project is maintained by [@mhuisi](https://github.com/mhuisi).
 See [the documentation of Lake](https://github.com/leanprover/lean4/blob/master/src/lake/README.md).
 
 ### Configuration
-Commands are configured with a lightweight DSL. The following declarations define a command `exampleCmd` with two subcommands `installCmd` and `testCmd`. `runExampleCmd` denotes a handler that is called when the command is run and is described further down below in the **Command Handlers** subsection.
+Commands are configured with a lightweight DSL. The following declarations define a command `exampleCmd` with two subcommands `installCmd` and `testCmd`.
+
+The signature-only `cli_def` generates a typed `exampleCmd.Parsed` wrapper struct with accessor functions for each flag and argument, and an `exampleCmd.mkCmd` constructor that takes a typed handler. The handler is then defined as a standalone function and attached via `mkCmd`.
 
 ```Lean
 open Cli
 
-def installCmd := `[Cli|
-  installCmd NOOP;
+cli_def installCmd NOOP;
   "installCmd provides an example for a subcommand without flags or arguments that does nothing. \
    Versions can be omitted."
-]
 
-def testCmd := `[Cli|
-  testCmd NOOP;
+cli_def testCmd NOOP;
   "testCmd provides another example for a subcommand without flags or arguments that does nothing."
-]
 
-def exampleCmd : Cmd := `[Cli|
-  exampleCmd VIA runExampleCmd; ["0.0.1"]
+cli_def exampleCmd; ["0.0.1"]
   "This string denotes the description of `exampleCmd`."
 
   FLAGS:
@@ -35,7 +32,7 @@ def exampleCmd : Cmd := `[Cli|
                                  which can be used to reference Lean modules like `Init.Data.Array` \
                                  or Lean files using a relative path like `Init/Data/Array.lean`."
     "set-paths" : Array String; "Declares a flag `--set-paths` \
-                                 that takes an argument of type `Array Nat`. \
+                                 that takes an argument of type `Array String`. \
                                  Quotation marks allow the use of hyphens."
 
   ARGS:
@@ -54,36 +51,35 @@ def exampleCmd : Cmd := `[Cli|
   EXTENSIONS:
     author "mhuisi";
     defaultValues! #[("priority", "0")]
-]
 ```
 
 ### Command handlers
-The command handler `runExampleCmd` demonstrates how to use the parsed user input.
+The command handler `runExampleCmd` demonstrates how to use the parsed input.
 
 ```Lean
-def runExampleCmd (p : Parsed) : IO UInt32 := do
-  let input   : String       := p.positionalArg! "input" |>.as! String
-  let outputs : Array String := p.variableArgsAs! String
-  IO.println <| "Input: " ++ input
-  IO.println <| "Outputs: " ++ toString outputs
+def runExampleCmd (p : exampleCmd.Parsed) : IO UInt32 := do
+  IO.println <| "Input: " ++ p.input
+  IO.println <| "Outputs: " ++ toString p.outputs
 
-  if p.hasFlag "verbose" then
+  if p.verbose then
     IO.println "Flag `--verbose` was set."
-  if p.hasFlag "invert" then
+  if p.invert then
     IO.println "Flag `--invert` was set."
-  if p.hasFlag "optimize" then
+  if p.optimize then
     IO.println "Flag `--optimize` was set."
 
-  let priority : Nat := p.flag! "priority" |>.as! Nat
+  let priority : Nat := p.priority?.getD 0
   IO.println <| "Flag `--priority` always has at least a default value: " ++ toString priority
 
-  if p.hasFlag "module" then
-    let moduleName : ModuleName := p.flag! "module" |>.as! ModuleName
+  if let some moduleName := p.module? then
     IO.println <| s!"Flag `--module` was set to `{moduleName}`."
 
-  if let some setPathsFlag := p.flag? "set-paths" then
-    IO.println <| toString <| setPathsFlag.as! (Array String)
+  if let some setPaths := p.setPaths? then
+    IO.println <| toString setPaths
+
   return 0
+
+def exampleCmd : Cmd := exampleCmd.mkCmd runExampleCmd
 ```
 
 ### Running the command
@@ -154,8 +150,8 @@ FLAGS:
                                 or Lean files using a relative path like
                                 `Init/Data/Array.lean`.
     --set-paths : Array String  Declares a flag `--set-paths` that takes an
-                                argument of type `Array String`. Quotation marks
-                                allow the use of hyphens.
+                                argument of type `Array String`. Quotation
+                                marks allow the use of hyphens.
 
 ARGS:
     input : String    Declares a positional argument <input> that takes an
@@ -173,7 +169,7 @@ SUBCOMMANDS:
 The full example can be found under `./CliTest/Example.lean`.
 
 ## Ad Hoc Documentation
-This section documents only the most common features of the library. For the full documentation, peek into `./Cli/Basic.lean` and `./Cli/Extensions.lean`! All definitions below live in the `Cli` namespace.
+This section documents only the most common features of the library. For the full documentation, peek into `./Cli/Basic.lean`, `./Cli/Typed.lean` and `./Cli/Extensions.lean`! All definitions below live in the `Cli` namespace.
 
 ```Lean
 -- In a `nameableStringArg`, string literals can either be used directly or an identifier can be
@@ -191,17 +187,30 @@ syntax variableArg := colGe "..." literalIdent " : " term "; " nameableStringArg
 
 syntax flag := colGe literalIdent ("," literalIdent)? (" : " term)? "; " nameableStringArg
 
-syntax "`[Cli|\n"
-    literalIdent runFun "; " ("[" nameableStringArg "]")?
+-- Untyped variant: generates `def <name> : Cmd` with the given handler or a no-op handler.
+-- Does not generate typed accessors.
+syntax "cli_def " literalIdent runFun "; " ("[" nameableStringArg "]")?
     nameableStringArg
     ("FLAGS:\n" withPosition((flag)*))?
     ("ARGS:\n" withPosition((positionalArg)* (variableArg)?))?
     ("SUBCOMMANDS: " sepBy(ident, ";", "; "))?
     ("EXTENSIONS: " sepBy(term, ";", "; "))?
-  "\n]" : term
-```
+  : command
+
+-- Typed variant: generates `<name>.Parsed` (a typed struct), accessors, and
+-- `<name>.mkCmd : (<name>.Parsed → IO UInt32) → Cmd`.
+-- With `RUN`: additionally generates `def <name> : Cmd := <name>.mkCmd <handler>`.
+-- Without `RUN`: the user defines their handler separately
+-- and attaches it via `def <name> : Cmd := <name>.mkCmd <handler>`.
+syntax "cli_def " literalIdent "; " ("[" nameableStringArg "]")?
+    nameableStringArg
+    ("FLAGS:\n" withPosition((flag)*))?
+    ("ARGS:\n" withPosition((positionalArg)* (variableArg)?))?
+    ("SUBCOMMANDS: " sepBy(ident, ";", "; "))?
+    ("EXTENSIONS: " sepBy(term, ";", "; "))?
+    (" RUN " term)?
+  : command
 
-```Lean
 /--
 Validates `args` by `Cmd.process?`ing the input according to `c`.
 Note that `args` designates the list `<foo>` in `somebinary <foo>`.
@@ -211,157 +220,5 @@ If neither of these flags were passed and processing was successful, the `run` h
 called command is executed.
 In the case of a processing error, the error is printed to stderr and an exit code of `1` is returned.
 -/
-def validate (c : Cmd) (args : List String) : IO UInt32 := do
-  let result := c.process args
-  match result with
-  | .ok (cmd, parsed) =>
-    if parsed.hasFlag "help" then
-      parsed.printHelp
-      return 0
-    if parsed.cmd.meta.hasVersion ∧ parsed.hasFlag "version" then
-      parsed.printVersion!
-      return 0
-    cmd.run parsed
-  | .error (cmd, err) =>
-    cmd.printError err
-    return 1
-```
-```Lean
-  /-- Represents parsed user input data. -/
-  structure Parsed where
-    /-- Recursive meta-data of the associated command. -/
-    cmd            : Parsed.Cmd
-    /-- Parent of the associated command. -/
-    parent?        : Option Parsed.Cmd
-    /-- Parsed flags. -/
-    flags          : Array Parsed.Flag
-    /-- Parsed positional arguments. -/
-    positionalArgs : Array Parsed.Arg
-    /-- Parsed variable arguments. -/
-    variableArgs   : Array Parsed.Arg
-    deriving Inhabited
-
-namespace Parsed
-  /-- Parent of the associated command. -/
-  def parent! (p : Parsed) : Parsed.Cmd
-
-  /-- Checks whether the associated command has a parent, i.e. whether it is not the root command. -/
-  def hasParent (p : Parsed) : Bool
-
-  /-- Finds the parsed flag in `p` with the corresponding `longName`. -/
-  def flag?          (p : Parsed) (longName : String) : Option Flag
-  /-- Finds the parsed positional argument in `p` with the corresponding `name`. -/
-  def positionalArg? (p : Parsed) (name : String)     : Option Arg
-
-  /-- Finds the parsed flag in `p` with the corresponding `longName`. -/
-  def flag!          (p : Parsed) (longName : String) : Flag
-  /-- Finds the parsed positional argument in `p` with the corresponding `name`. -/
-  def positionalArg! (p : Parsed) (name : String)     : Arg
-
-  /-- Checks whether `p` has a parsed flag with the corresponding `longName`. -/
-  def hasFlag          (p : Parsed) (longName : String) : Bool
-  /-- Checks whether `p` has a positional argument with the corresponding `longName`. -/
-  def hasPositionalArg (p : Parsed) (name : String)     : Bool
-
-  /--
-  Converts all `p.variableArgs` values to `τ`, which should be the same type
-  that was designated in the corresponding `Cli.Arg`.
-  Yields `none` if the conversion was unsuccessful, which can only
-  happen if `τ` is not the same type as the one designated in the corresponding `Cli.Arg`.
-  -/
-  def variableArgsAs? (p : Parsed) (τ) [ParseableType τ] : Option (Array τ)
-
-  /--
-  Converts all `p.variableArgs` values to `τ`, which should be the same type
-  that was designated in the corresponding `Cli.Arg`.
-  Panics if the conversion was unsuccessful, which can only
-  happen if `τ` is not the same type as the one designated in the corresponding `Cli.Arg`.
-  -/
-  def variableArgsAs! (p : Parsed) (τ) [Inhabited τ] [ParseableType τ] : Array τ
-end Parsed
-```
-```Lean
-namespace Parsed
-  /--
-  Represents a flag and its parsed value.
-  Use `Parsed.Flag.as!` to convert the value to some `ParseableType`.
-  -/
-  structure Flag where
-    /-- Associated flag meta-data. -/
-    flag  : Flag
-    /-- Parsed value that was validated and conforms to `flag.type`. -/
-    value : String
-
-  namespace Flag
-    /--
-    Converts `f.value` to `τ`, which should be the same type
-    that was designated in `f.flag.type`.
-    Yields `none` if the conversion was unsuccessful, which can only
-    happen if `τ` is not the same type as the one designated in `f.flag.type`.
-    -/
-    def as? (f : Flag) (τ) [ParseableType τ] : Option τ
-    /--
-    Converts `f.value` to `τ`, which should be the same type
-    that was designated in `f.flag.type`.
-    Panics if the conversion was unsuccessful, which can only
-    happen if `τ` is not the same type as the one designated in `f.flag.type`.
-    -/
-    def as! (f : Flag) (τ) [Inhabited τ] [ParseableType τ] : τ
-  end Flag
-
-  /--
-  Represents an argument and its parsed value.
-  Use `Parsed.Arg.as!` to convert the value to some `ParseableType`.
-  -/
-  structure Arg where
-    /-- Associated argument meta-data. -/
-    arg   : Arg
-    /-- Parsed value that was validated and conforms to `arg.type`. -/
-    value : String
-
-  namespace Arg
-    /--
-    Converts `a.value` to `τ`, which should be the same type
-    that was designated in `a.arg.type`.
-    Yields `none` if the conversion was unsuccessful, which can only
-    happen if `τ` is not the same type as the one designated in `a.arg.type`.
-    -/
-    def as? (a : Arg) (τ) [ParseableType τ] : Option τ
-    /--
-    Converts `a.value` to `τ`, which should be the same type
-    that was designated in `a.arg.type`.
-    Panics if the conversion was unsuccessful, which can only
-    happen if `τ` is not the same type as the one designated in `a.arg.type`.
-    -/
-    def as! (a : Arg) (τ) [Inhabited τ] [ParseableType τ] : τ
-  end Arg
-end Parsed
-```
-```Lean
-/--
-Creates a new command. Adds a `-h, --help` and a `--version` flag if a version is designated.
-Updates the `parentNames` of all subcommands.
-- `name`:                Name that is displayed in the help.
-- `version?`:            Version that is displayed in the help and when the version is queried.
-- `description`:         Description that is displayed in the help.
-- `furtherInformation?`: Information appended to the end of the help. Useful for command extensions.
-- `flags`:               Supported flags ("options" in standard terminology).
-- `positionalArgs`:      Supported positional arguments ("operands" in standard terminology).
-- `variableArg?`:        Variable argument at the end of the positional arguments.
-- `run`:                 Handler to run when the command is called and flags/arguments have been successfully processed.
-- `subCmds`:             Subcommands.
-- `extension?`:          Extension of the Cli library.
--/
-def mk
-  (name                : String)
-  (version?            : Option String)
-  (description         : String)
-  (furtherInformation? : Option String := none)
-  (flags               : Array Flag    := #[])
-  (positionalArgs      : Array Arg     := #[])
-  (variableArg?        : Option Arg    := none)
-  (run                 : Parsed → IO UInt32)
-  (subCmds             : Array Cmd        := #[])
-  (extension?          : Option Extension := none)
-  : Cmd
+def validate (c : Cmd) (args : List String) : IO UInt32
 ```