Documentation

Mathlib.Lean.Name

Additional functions on Lean.Name. #

We provide allNames and allNamesByModule.

Retrieve all names in the environment satisfying a predicate.

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

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

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

      Decapitalize the last component of a name.

      Equations
      • n.decapitalize = n.modifyBase fun (x : Lean.Name) => match x with | p.str s => p.str s.decapitalize | n => n
      Instances For

        Whether the lemma has a name of the form produced by Lean.Meta.mkAuxLemma.

        Equations
        • n.isAuxLemma = match n with | (pre.str "_auxLemma").num i => true | x => false
        Instances For

          Unfold all lemmas created by Lean.Meta.mkAuxLemma. The names of these lemmas end in _auxLemma.nn where nn is a number.

          Equations
          Instances For