Documentation

Lean.Compiler.ImplementedByAttr

@[export lean_get_implemented_by]
Instances For
    def Lean.setImplementedBy {m : TypeType} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (declName : Lake.Name) (impName : Lake.Name) :
    Instances For