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