Skip to content

Commit

Permalink
feat: add qualifiers for Arg and Flag to disambiguate Cli.{Parsed.}Flag
Browse files Browse the repository at this point in the history
Thanks to leanprover/lean4#5783,
we now have recursive structure commands,
which trips the inference into constructing a recursive struct.
Therefore, we disambiguate the fields in `Cli.Parsed.Flag` to explicitly refer to `Cli.Flag`.

Discovered when bumping toolchain to nightly in leanprover/LNSym#244.
  • Loading branch information
bollu committed Nov 1, 2024
1 parent 2cf1030 commit d8545d4
Showing 1 changed file with 4 additions and 3 deletions.
7 changes: 4 additions & 3 deletions Cli/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -340,6 +340,7 @@ section Configuration
def isParamless (f : Flag) : Bool := f.type == Unit
end Flag


/--
Represents an argument (either positional or variable),
usually known as "operand" in standard terminology
Expand All @@ -360,7 +361,7 @@ section Configuration
-/
structure Flag where
/-- Associated flag meta-data. -/
flag : Flag
flag : Cli.Flag
/-- Parsed value that was validated and conforms to `flag.type`. -/
value : String
deriving Inhabited, BEq, Repr
Expand Down Expand Up @@ -393,7 +394,7 @@ section Configuration
-/
structure Arg where
/-- Associated argument meta-data. -/
arg : Arg
arg : Cli.Arg
/-- Parsed value that was validated and conforms to `arg.type`. -/
value : String
deriving Inhabited, BEq, Repr
Expand Down Expand Up @@ -1630,4 +1631,4 @@ section IO
end Cmd
end IO

end Cli
end Cli

0 comments on commit d8545d4

Please sign in to comment.