diff --git a/src/Init/Lean/Data/Name.lean b/src/Init/Lean/Data/Name.lean index 7560b0c86b..5a67bfddc7 100644 --- a/src/Init/Lean/Data/Name.lean +++ b/src/Init/Lean/Data/Name.lean @@ -27,6 +27,13 @@ def getPrefix : Name → Name | str p s _ => p | num p s _ => p +def getRoot : Name → Name +| anonymous => anonymous +| n@(str anonymous _ _) => n +| n@(num anonymous _ _) => n +| str n _ _ => getRoot n +| num n _ _ => getRoot n + def getNumParts : Name → Nat | anonymous => 0 | str p _ _ => getNumParts p + 1 diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean index 228bd4cb8c..9ff5ada99a 100644 --- a/src/Init/Lean/Elab/Syntax.lean +++ b/src/Init/Lean/Elab/Syntax.lean @@ -153,10 +153,14 @@ pure kind private def elabKind (stx : Syntax) (catName : Name) : CommandElabM Name := do if stx.isNone then mkFreshKind catName -else do +else let kind := stx.getIdAt 1; - currNamespace ← getCurrNamespace; - pure (currNamespace ++ kind) + if kind.getRoot == `_kind then + -- unique fresh kind, do not qualify + pure kind + else do + currNamespace ← getCurrNamespace; + pure (currNamespace ++ kind) @[builtinCommandElab «syntax»] def elabSyntax : CommandElab := fun stx => do diff --git a/tests/lean/run/macro2.lean b/tests/lean/run/macro2.lean index 05e25da33d..519b1cd15a 100644 --- a/tests/lean/run/macro2.lean +++ b/tests/lean/run/macro2.lean @@ -2,6 +2,9 @@ new_frontend notation a `**`:50 b:50 => b * a * b notation "~" a => a+a +namespace Foo +notation "~~" a => a+a +end Foo syntax term "+++":60 term:59 : term