instance Lean.NameSet.instSingletonName_batteries : Singleton Name NameSet

Equations

• Lean.NameSet.instSingletonName_batteries = { singleton := fun (n : Lean.Name) => ∅.insert n }

instance Lean.NameSet.instUnion_batteries : Union NameSet

Equations

• Lean.NameSet.instUnion_batteries = { union := fun (s t : Lean.NameSet) => Lean.RBTree.fold (fun (t : Lean.NameSet) (n : Lean.Name) => t.insert n) t s }

instance Lean.NameSet.instInter_batteries : Inter NameSet

Equations

• Lean.NameSet.instInter_batteries = { inter := fun (s t : Lean.NameSet) => Lean.RBTree.fold (fun (r : Lean.NameSet) (n : Lean.Name) => if t.contains n = true then r.insert n else r) ∅ s }

instance Lean.NameSet.instSDiff_batteries : SDiff NameSet

Equations

• Lean.NameSet.instSDiff_batteries = { sdiff := fun (s t : Lean.NameSet) => Lean.RBTree.fold (fun (s : Lean.NameSet) (n : Lean.Name) => Lean.RBTree.erase s n) s t }

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

• Lean.NameSet.ofList l = List.foldl (fun (s : Lean.NameSet) (n : Lean.Name) => s.insert n) ∅ l

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

• Lean.NameSet.ofArray a = Array.foldl (fun (s : Lean.NameSet) (n : Lean.Name) => s.insert n) ∅ a