From 8b9060b33f1c774a80bd9c53456ca40e0f2fe89d Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 14 Oct 2026 08:39:34 +0000 Subject: [PATCH 1/3] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 941714a1c..770d5ec02 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-10-05 +leanprover/lean4-pr-releases:pr-release-15682-4ee966c From 4190d4202bd6218b1575c005246badc661f65320 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 19 Oct 2026 09:52:26 +0000 Subject: [PATCH 2/3] fix: reference-manual messages after lean4#15682 elaborates the do continuation once --- reference-manual/Manual/NotationsMacros.lean | 8 -------- 1 file changed, 8 deletions(-) diff --git a/reference-manual/Manual/NotationsMacros.lean b/reference-manual/Manual/NotationsMacros.lean index 203cc7f2a..f01cb11f4 100644 --- a/reference-manual/Manual/NotationsMacros.lean +++ b/reference-manual/Manual/NotationsMacros.lean @@ -1200,14 +1200,6 @@ info: TSyntax `str info: TSyntax Name.anonymous --- info: Syntax.TSepArray `num "," ---- -info: Syntax.TSepArray `num "," ---- -info: TSyntax Name.anonymous ---- -info: Syntax.TSepArray `num "," ---- -info: Syntax.TSepArray `num "," -/ #check_msgs in macro "gah!" thing:str other:(str <|> num) arg:num,* : term => do From f0ecdd919ab933ea2aff3b43603188b84cabbd3f Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Mon, 19 Oct 2026 10:07:43 +0000 Subject: [PATCH 3/3] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index c51720493..0ebb579f8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-10-17 +leanprover/lean4-pr-releases:pr-release-15682-f65bf27