Merge pull request #35 from leanprover/bump_toolchain_to_v4.15.0-rc1

chore: bump toolchain to v4.15.0-rc1
leanprover · Dec 2, 2024 · 03b5086 · 03b5086
2 parents bee437b + 47f4bc1
commit 03b5086
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git 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`. -/

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0
+leanprover/lean4:v4.15.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.14.0
		leanprover/lean4:v4.15.0-rc1