HepLean Documentation

Lean.Linter.ConstructorAsVariable

A linter that warns when bound variable names are the same as constructor names for their types, modulo namespaces.

Reports when bound variables' names overlap with constructor names for their type. This is to warn especially new users that they have built a pattern that matches anything, rather than one that matches a particular constructor. Use linter.constructorNameAsVariable to disable.

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