From aee63ee7b0a7ab41e285ad1f56e708da8337b7dc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Nov 2022 06:39:49 -0800 Subject: [PATCH] feat: panic at `Name.append` if both names have macro scopes --- src/Init/Prelude.lean | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index e516444b4a..e6a60a86be 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -4202,12 +4202,7 @@ If `a` has macro scopes, then the are propagated to result of `append a b` def Name.append (a b : Name) : Name := match a.hasMacroScopes, b.hasMacroScopes with | true, true => - /- - TODO: this case should be unreachable. Many interactive tests reach this code. We should fix them. - The following workaround erases `b`s macro scopes and keeps the one from `a`. - -/ - let view := extractMacroScopes a - { view with name := appendCore view.name b.eraseMacroScopes }.review + panic "Error: invalid `Name.append`, both arguments have macro scopes, consider using `eraseMacroScopes`" | true, false => let view := extractMacroScopes a { view with name := appendCore view.name b }.review