From dbe7078e80fd2c7c28746983d95304ea3ce4cacf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Jun 2019 17:24:16 -0700 Subject: [PATCH] feat(library/init/lean/attributes): add `ParametricAttribute.setParam` --- library/init/lean/attributes.lean | 8 ++++++++ 1 file changed, 8 insertions(+) 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