From 9b0aba6a69f90d19b97f7e3dfdb731d3330e382d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 10 Jul 2026 11:57:08 +0000 Subject: [PATCH 1/2] fix: enforce set notation per-element indentation --- src/Init/NotationExtra.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index bf509c6872bc..0d50763c1cd6 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -335,7 +335,7 @@ macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term => end Lean /-- `{ a, b, c }` syntax, powered by the `Singleton` and `Insert` typeclasses. -/ -syntax "{" term,+ "}" : term +syntax "{" withPosition(term),+ "}" : term macro_rules | `({$x:term}) => `(singleton $x) From 1ecc0582b585296031335aad36668e6fe0453c2f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 10 Jul 2026 13:46:15 +0000 Subject: [PATCH 2/2] doc --- src/Init/NotationExtra.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 0d50763c1cd6..403cc1578424 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -335,6 +335,15 @@ macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term => end Lean /-- `{ a, b, c }` syntax, powered by the `Singleton` and `Insert` typeclasses. -/ +/- +We use `withPosition` despite the parenthesized context because +``` +{ aaa + bbb } +``` +otherwise could be either a two-field structure or a singleton set, which seems way too confusing +even when the elaborator can disambiguate the two. +-/ syntax "{" withPosition(term),+ "}" : term macro_rules