opaque Lean.Compiler.implementedByAttr : ParametricAttribute Name

@[export lean_get_implemented_by]

def Lean.Compiler.getImplementedBy? (env : Environment) (declName : Name) : Option Name

Equations

• Lean.Compiler.getImplementedBy? env declName = Lean.Compiler.implementedByAttr.getParam? env declName

def Lean.Compiler.setImplementedBy (env : Environment) (declName impName : Name) : Except String Environment

Equations

• Lean.Compiler.setImplementedBy env declName impName = Lean.Compiler.implementedByAttr.setParam env declName impName

def Lean.setImplementedBy {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (declName impName : Name) : m Unit

Equations

• One or more equations did not get rendered due to their size.