From 0a0e1036b9127a0f8b1cb9019a0694a266e5be50 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 1 Nov 2024 13:35:27 -0500 Subject: [PATCH] feat: add qualifiers for Arg and Flag to disambiguate Cli.{Parsed.}Flag Thanks to https://github.com/leanprover/lean4/pull/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 https://github.com/leanprover/LNSym/pull/244. --- Cli/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Cli/Basic.lean b/Cli/Basic.lean index b12f2d3..03307c4 100644 --- a/Cli/Basic.lean +++ b/Cli/Basic.lean @@ -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 @@ -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 @@ -1630,4 +1630,4 @@ section IO end Cmd end IO -end Cli \ No newline at end of file +end Cli