diff --git a/library/init/lean/attributes.lean b/library/init/lean/attributes.lean
index bca456a8a9..8d225c0bda 100644
--- a/library/init/lean/attributes.lean
+++ b/library/init/lean/attributes.lean
@@ -325,6 +325,14 @@ match env.getModuleIdxFor decl with
   | none          := none
 | none        := (attr.ext.getState env).find decl
 
+def setParam {α : Type} (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment :=
+if (env.getModuleIdxFor decl).isNone then
+  Except.error ("invalid '" ++ toString attr.attr.name ++ "'.setParam, declaration is in an imported module")
+else if ((attr.ext.getState env).find decl).isSome then
+  Except.error ("invalid '" ++ toString attr.attr.name ++ "'.setParam, attribute has already been set")
+else
+  Except.ok (attr.ext.addEntry env (decl, param))
+
 end ParametricAttribute
 
 end Lean