Documentation

Mathlib.Lean.Name

Additional functions on Lean.Name. #

We provide Name.getModule, and allNames and allNamesByModule.

Retrieve all names in the environment satisfying a predicate.

Instances For

    Retrieve all names in the environment satisfying a predicate, gathered together into a HashMap according to the module they are defined in.

    Instances For

      Returns the very first part of a name: for Mathlib.Data.Set.Basic it returns Mathlib.

      Equations
      Instances For