From 3fec40dbf0be4ce601f8499605fe05217dc24b5b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Dec 2024 13:34:10 +1100 Subject: [PATCH 1/2] chore: bump toolchain to v4.15.0-rc1 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 1e70935..cf25a98 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.14.0 +leanprover/lean4:v4.15.0-rc1 From 47f4bc188869f5d066118e031def245e8b47aac3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 2 Dec 2024 13:36:58 +1100 Subject: [PATCH 2/2] fix --- Lean4CheckerTests/OpenPrivate.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Lean4CheckerTests/OpenPrivate.lean b/Lean4CheckerTests/OpenPrivate.lean index 7ade0b9..95b2cc2 100644 --- a/Lean4CheckerTests/OpenPrivate.lean +++ b/Lean4CheckerTests/OpenPrivate.lean @@ -99,7 +99,7 @@ name component. It is also possible to specify the module instead with `open private a b c from Other.Module`. -/ -syntax (name := openPrivate) "open private" (ppSpace ident)* +syntax (name := openPrivate) "open" "private" (ppSpace ident)* (" in" (ppSpace ident)*)? (" from" (ppSpace ident)*)? : command /-- Elaborator for `open private`. -/ @@ -119,7 +119,7 @@ It will also open the newly created alias definition under the provided short na It is also possible to specify the module instead with `export private a b c from Other.Module`. -/ -syntax (name := exportPrivate) "export private" (ppSpace ident)* +syntax (name := exportPrivate) "export" "private" (ppSpace ident)* (" in" (ppSpace ident)*)? (" from" (ppSpace ident)*)? : command /-- Elaborator for `export private`. -/