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