Documentation

Mathlib.Util.LongNames

Commands #long_names and #long_instances #

For finding declarations with excessively long names.

source
def printNameHashMap (h : Std.HashMap Lean.Name (Array Lean.Name)) :
IO Unit

Helper function for #long_names and #long_instances.

Equations
  • One or more equations did not get rendered due to their size.
source
def «command#long_names_» :
Lean.ParserDescr

Lists all declarations with a long name, gathered according to the module they are defined in. Use as #long_names or #long_names 100 to specify the length.

Equations
  • One or more equations did not get rendered due to their size.
source
def «command#long_instances_» :
Lean.ParserDescr

Lists all instances with a long name beginning with inst, gathered according to the module they are defined in. This is useful for finding automatically named instances with absurd names.

Use as #long_names or #long_names 100 to specify the length.

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