test

leanprover · Oct 2, 2024 · 55f5968 · 55f5968
1 parent 82a5ec1
commit 55f5968
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/tests/lean/run/hashmap.lean b/tests/lean/run/hashmap.lean
@@ -382,6 +382,10 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do
 #guard_msgs in
 #eval m.toArray
 
+/-- info: Std.HashSet.Raw.ofList [1000000000, 2, 1, 16] -/
+#guard_msgs in
+#eval m ∪ {16, 16}
+
 /-- info: [1000000000, 2, 1, 16] -/
 #guard_msgs in
 #eval (m.insertMany [16, 16]).toList