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

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

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