def Batteries.Tactic.Lint.impossibleInstance : Linter

Lints for instances with arguments that cannot be filled in, like

instance {α β : Type} [Group α] : Mul α where ...

Equations

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

def Batteries.Tactic.Lint.nonClassInstance : Linter

A linter for checking if any declaration whose type is not a class is marked as an instance.

Equations

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