@[implicit_reducible]

instance Lean.NameSet.instSingletonName_batteries : Singleton Name NameSet

Equations

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

@[implicit_reducible]

instance Lean.NameSet.instUnion_batteries : Union NameSet

Equations

• Lean.NameSet.instUnion_batteries = { union := fun (s t : Lean.NameSet) => Std.TreeSet.foldl (fun (t : Lean.NameSet) (n : Lean.Name) => t.insert n) t s }

@[implicit_reducible]

instance Lean.NameSet.instInter_batteries : Inter NameSet

Equations

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

@[implicit_reducible]

instance Lean.NameSet.instSDiff_batteries : SDiff NameSet

Equations

• Lean.NameSet.instSDiff_batteries = { sdiff := fun (s t : Lean.NameSet) => Std.TreeSet.foldl (fun (s : Lean.NameSet) (n : Lean.Name) => Std.TreeSet.erase s n) s t }