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.
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.