opaque Lean.Compiler.implementedByAttr : Lean.ParametricAttribute Lake.Name

@[export lean_get_implemented_by]

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

Equations

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

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

Equations

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

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

Equations

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