diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 8d3354fc0338..e9bc2632ac30 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -4335,8 +4335,13 @@ def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name := Name.mkNum (Name.mkStr (Name.appendCore (Name.mkStr n "_@") mainModule) "_hyg") scp /-- -Append two names that may have macro scopes. The macro scopes in `b` are always erased. -If `a` has macro scopes, then they are propagated to the result of `append a b`. +Appends two names `a` and `b`, propagating macro scopes from `a` or `b`, if any, to the result. +Panics if both `a` and `b` have macro scopes. + +This function is used for the `Append Name` instance. + +See also `Lean.Name.appendCore`, which appends names without any consideration for macro scopes. +Also consider `Lean.Name.eraseMacroScopes` to erase macro scopes before appending, if appropriate. -/ def Name.append (a b : Name) : Name := match a.hasMacroScopes, b.hasMacroScopes with diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index 34c800fb48e8..91bef0d99b6e 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -404,7 +404,7 @@ where for _ in [:revComponents.length] do match revComponents with | [] => return none - | cmpt::rest => candidate := cmpt ++ candidate; revComponents := rest + | cmpt::rest => candidate := Name.appendCore cmpt candidate; revComponents := rest match (ā† resolveGlobalName candidate) with | [(potentialMatch, _)] => if potentialMatch == nā‚€ then return some candidate else continue | _ => continue diff --git a/tests/lean/run/2291.lean b/tests/lean/run/2291.lean new file mode 100644 index 000000000000..0390315bd03c --- /dev/null +++ b/tests/lean/run/2291.lean @@ -0,0 +1,8 @@ +/-! +Issue #2291 + +The following example would cause the pretty printer to panic. +-/ + +set_option trace.compiler.simp true in +#eval [0]