ink

def Std.Tactic.Lint.impossibleInstance : Std.Tactic.Lint.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.

ink

def Std.Tactic.Lint.dangerousInstance : Std.Tactic.Lint.Linter

Lints for instances that produce subgoals with metavariables, like

instance [Group β] : Add α where ...

Equations

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