Documentation

Batteries.Data.NameSet

source
instance Lean.NameSet.instSingletonName_batteries :
Singleton Name NameSet
Equations
    source
    instance Lean.NameSet.instUnion_batteries :
    Union NameSet
    Equations
      source
      instance Lean.NameSet.instInter_batteries :
      Inter NameSet
      Equations
        source
        instance Lean.NameSet.instSDiff_batteries :
        SDiff NameSet
        Equations
          source
          def Lean.NameSet.ofList (l : List Name) :
          NameSet

          Create a Lean.NameSet from a List. This operation is O(n) in the length of the list.

          Equations
            Instances For
              source
              def Lean.NameSet.ofArray (a : Array Name) :
              NameSet

              Create a Lean.NameSet from an Array. This operation is O(n) in the size of the array.

              Equations
                Instances For