fix: allow builtin simprocs to be deleted even when we have not impor…

…ted the file defining them

src/Lean/Elab/Declaration.lean

@@ -347,7 +347,21 @@ def elabMutual : CommandElab := fun stx => do
   let attrs ← elabAttrs attrInsts
   let idents := stx[4].getArgs
   for ident in idents do withRef ident <| liftTermElabM do
-    let declName ← resolveGlobalConstNoOverloadWithInfo ident
+    /-
+    HACK to allow `attribute` command to disable builtin simprocs.
+    TODO: find a better solution. Example: have some "fake" declaration
+    for builtin simprocs.
+    -/
+    let declNames ←
+       try
+         resolveGlobalConst ident
+       catch _ =>
+         let name := ident.getId.eraseMacroScopes
+         if (← Simp.isBuiltinSimproc name) then
+           pure [name]
+         else
+           throwUnknownConstant name
+    let declName ← ensureNonAmbiguous ident declNames
     Term.applyAttributes declName attrs
     for attrName in toErase do
       Attribute.erase declName attrName

tests/lean/run/simproc_builtin_erase.lean

@@ -0,0 +1,12 @@
+example (h : 12 = x) : 10 + 2 = x := by
+  simp
+  guard_target =ₛ 12 = x
+  assumption
+
+attribute [-simp] Nat.reduceAdd
+
+example (h : 12 = x) : 10 + 2 = x := by
+  fail_if_success simp
+  simp [Nat.reduceAdd]
+  guard_target =ₛ 12 = x
+  assumption