fix: allow multiple declareBuiltin per declaration

leanprover · May 23, 2024 · dfb496a · dfb496a
1 parent 2509941
commit dfb496a
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.AddDecl
+import Lean.MonadEnv
 import Lean.Elab.InfoTree.Main
 
 namespace Lean
@@ -139,7 +140,7 @@ def setBuiltinInitAttr (env : Environment) (declName : Name) (initFnName : Name
   builtinInitAttr.setParam env declName initFnName
 
 def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit := do
-  let name := `_regBuiltin ++ forDecl
+  let name ← mkAuxName (`_regBuiltin ++ forDecl) 1
   let type := mkApp (mkConst `IO) (mkConst `Unit)
   let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque,
                                      safety := DefinitionSafety.safe }