fix: update for lean4#5842 (#19)

Now the structure being defined is available as a local variable, so some structure fields need to be qualified.
leanprover · Oct 28, 2024 · 039d23a · 039d23a
1 parent bf066c3
commit 039d23a
Showing 1 changed file with 3 additions and 3 deletions.
diff --git 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
+end Cli