From f9054125e9ab4f9cc3ea9f7ce6cb0ad3c18cdd06 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 4 Nov 2024 12:08:02 +1100 Subject: [PATCH] chore: adaptations for v4.14.0-rc1 --- Cli/Basic.lean | 8 ++++---- lean-toolchain | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Cli/Basic.lean b/Cli/Basic.lean index b12f2d3..a3e50f4 100644 --- a/Cli/Basic.lean +++ b/Cli/Basic.lean @@ -256,7 +256,7 @@ section Configuration parse? s := do if s == ".lean" then none - let name := + let name := if s.endsWith ".lean" then let pathComponents := (s : FilePath).withExtension "" |>.components pathComponents.foldl .mkStr .anonymous @@ -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 diff --git a/lean-toolchain b/lean-toolchain index 4ef27c4..0bef727 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.9.0 +leanprover/lean4:v4.14.0-rc1