Documentation

Mathlib.Util.LongNames

Commands #long_names and #long_instances #

For finding declarations with excessively long names.

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

Helper function for #long_names and #long_instances.

Instances For
    source
    🔸 coverage
    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.

    Instances For
      source
      🔸 coverage
      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.

      Instances For