@[export lean_get_implemented_by]
Equations
Instances For
Equations
Instances For
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.