source
opaque Lean.Linter.linter.suspiciousUnexpanderPatterns :
Lean.Option Bool
source
def Lean.Linter.getLinterSuspiciousUnexpanderPatterns (o : LinterOptions) :
Bool
Equations

- Lean.Linter.getLinterSuspiciousUnexpanderPatterns o = Lean.Linter.getLinterValue Lean.Linter.linter.suspiciousUnexpanderPatterns o

Instances For

source
def Lean.Linter.suspiciousUnexpanderPatterns :
Linter
Equations

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

Instances For