chore: set notation for Lean.HashSet (#448)

leanprover-community · Dec 14, 2023 · 6b4cf96 · 6b4cf96
1 parent 3bb8c37
commit 6b4cf96
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Std/Lean/HashSet.lean b/Std/Lean/HashSet.lean
@@ -5,11 +5,15 @@ Authors: Jannis Limperg
 -/
 
 import Lean.Data.HashSet
+import Std.Classes.SetNotation
 
 namespace Lean.HashSet
 
 variable [BEq α] [Hashable α]
 
+instance : Singleton α (HashSet α) := ⟨fun x => HashSet.empty.insert x⟩
+instance : Insert α (HashSet α) := ⟨fun a s => s.insert a⟩
+
 /--
 `O(n)`. Returns `true` if `f` returns `true` for any element of the set.
 -/