opaque Lean.Compiler.implementedByAttr : ParametricAttribute Name

@[export lean_get_implemented_by]

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

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

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