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 0a0e103
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions Cli/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -360,7 +360,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 +393,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 +1630,4 @@ section IO
end Cmd
end IO

end Cli
end Cli

0 comments on commit 0a0e103

Please sign in to comment.