Equations
- Lean.Compiler.getImplementedBy env declName = Lean.ParametricAttribute.getParam Lean.Compiler.implementedByAttr env declName
def
Lean.Compiler.setImplementedBy
(env : Lean.Environment)
(declName : Lean.Name)
(impName : Lean.Name)
:
Equations
- Lean.Compiler.setImplementedBy env declName impName = Lean.ParametricAttribute.setParam Lean.Compiler.implementedByAttr env declName impName
def
Lean.setImplementedBy
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadEnv m]
[inst : Lean.MonadError m]
(declName : Lean.Name)
(impName : Lean.Name)
:
m Unit
Equations
- Lean.setImplementedBy declName impName = do let env ← Lean.getEnv match Lean.Compiler.setImplementedBy env declName impName with | Except.ok env => Lean.setEnv env | Except.error ex => Lean.throwError (Function.comp Lean.MessageData.ofFormat Lean.format ex)