max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/attributes): add ParametricAttribute.setParam

Browse source
This commit is contained in:
Leonardo de Moura 2019-06-18 17:24:16 -07:00
parent 0dfca42f6d
commit dbe7078e80
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/lean/attributes.lean
View file

@ -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