From 1dcffe57141d453bc85a1b0c99ac2c651be5dc91 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 31 Aug 2020 11:05:37 -0700 Subject: [PATCH] feat: add `setImplementedBy` --- src/Lean/Compiler/ImplementedByAttr.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean index 4bd2f3c30b..166b438a56 100644 --- a/src/Lean/Compiler/ImplementedByAttr.lean +++ b/src/Lean/Compiler/ImplementedByAttr.lean @@ -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