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

feat: add setImplementedBy

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-31 11:05:37 -07:00
parent 9f16d01058
commit 1dcffe5714
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Compiler/ImplementedByAttr.lean
View file

@ -22,8 +22,11 @@ registerParametricAttribute `implementedBy "name of the Lean (probably unsafe) f
constant implementedByAttr : ParametricAttribute Name := arbitrary _
@[export lean_get_implemented_by]
def getImplementedBy (env : Environment) (n : Name) : Option Name :=
implementedByAttr.getParam env n
def getImplementedBy (env : Environment) (declName : Name) : Option Name :=
implementedByAttr.getParam env declName
def setImplementedBy (env : Environment) (declName : Name) (impName : Name) : Except String Environment :=
implementedByAttr.setParam env declName impName
end Compiler
end Lean