Documentation

Lean.Data.NameMap

Equations
Instances For
    Equations
    Instances For
      def Lean.NameMap.find? {α : Type} (m : Lake.NameMap α) (n : Lake.Name) :
      Equations
      Instances For
        instance Lean.NameMap.instForInProdName {α : Type} {m : Type u_1 → Type u_2} :
        Equations
        Equations
        Instances For
          Equations
          Instances For

            The union of two NameSets.

            Equations
            Instances For
              @[reducible, inline]
              Equations
              Instances For
                @[reducible, inline]
                Equations
                Instances For
                  @[reducible, inline]
                  Equations
                  Instances For
                    @[inline]
                    Equations
                    Instances For
                      Equations
                      Instances For
                        Equations
                        • v₁.isPrefixOf v₂ = (v₁.name.isPrefixOf v₂.name && v₁.scopes == v₂.scopes && v₁.mainModule == v₂.mainModule && v₁.imported == v₂.imported)
                        Instances For
                          Equations
                          • v₁.isSuffixOf v₂ = (v₁.name.isSuffixOf v₂.name && v₁.scopes == v₂.scopes && v₁.mainModule == v₂.mainModule && v₁.imported == v₂.imported)
                          Instances For