feat: reverse HashMap.toList, so it agrees with HashMap.toArray (#6244)
This PR changes the implementation of `HashMap.toList`, so the ordering agrees with `HashMap.toArray`. Currently there are no verification lemmas about `HashMap.toList`, so no contract is being broken yet!
This commit is contained in:
Kim Morrison
GitHub
parent
24b412ebe3
commit
7b98fbece4
5 changed files with 106 additions and 48 deletions
|
|
@ -10,6 +10,11 @@ import Init.NotationExtra
|
|||
This is an internal implementation file of the hash map. Users of the hash map should not rely on
|
||||
the contents of this file.
|
||||
|
||||
Note that some functions in this file (in particular, `foldrM`, `foldr`, `toList`, `replace`, and
|
||||
`erase`) are not tail-recursive. This is not a problem because they are only used internally by
|
||||
`HashMap`, where `AssocList` is always small. Before making this API public, we would need to add
|
||||
`@[csimp]` lemmas for tail-recursive implementations.
|
||||
|
||||
File contents: Operations on associative lists
|
||||
-/
|
||||
|
||||
|
|
@ -46,6 +51,17 @@ namespace AssocList
|
|||
@[inline] def foldl (f : δ → (α : α) → β α → δ) (init : δ) (as : AssocList α β) : δ :=
|
||||
Id.run (foldlM f init as)
|
||||
|
||||
/-- Internal implementation detail of the hash map -/
|
||||
@[specialize] def foldrM (f : (a : α) → β a → δ → m δ) : (init : δ) → AssocList α β → m δ
|
||||
| d, nil => pure d
|
||||
| d, cons a b es => do
|
||||
let d ← foldrM f d es
|
||||
f a b d
|
||||
|
||||
/-- Internal implementation detail of the hash map -/
|
||||
@[inline] def foldr (f : (a : α) → β a → δ → δ) (init : δ) (as : AssocList α β) : δ :=
|
||||
Id.run (foldrM f init as)
|
||||
|
||||
/-- Internal implementation detail of the hash map -/
|
||||
@[inline] def forM (f : (a : α) → β a → m PUnit) (as : AssocList α β) : m PUnit :=
|
||||
as.foldlM (fun _ => f) ⟨⟩
|
||||
|
|
|
|||
|
|
@ -204,4 +204,9 @@ theorem foldl_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a
|
|||
(l.toList.map (fun p => f p.1 p.2)).reverse ++ acc := by
|
||||
induction l generalizing acc <;> simp_all [AssocList.foldl, AssocList.foldlM, Id.run]
|
||||
|
||||
theorem foldr_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) :
|
||||
l.foldr (fun k v acc => f k v :: acc) acc =
|
||||
(l.toList.map (fun p => f p.1 p.2)) ++ acc := by
|
||||
induction l generalizing acc <;> simp_all [AssocList.foldr, AssocList.foldrM, Id.run]
|
||||
|
||||
end Std.DHashMap.Internal.AssocList
|
||||
|
|
|
|||
|
|
@ -83,12 +83,36 @@ theorem fold_cons_key {l : Raw α β} {acc : List α} :
|
|||
l.fold (fun acc k _ => k :: acc) acc = List.keys (toListModel l.buckets).reverse ++ acc := by
|
||||
rw [fold_cons_apply, keys_eq_map, map_reverse]
|
||||
|
||||
theorem foldRev_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
|
||||
l.foldRev f init = l.buckets.foldr (fun l acc => l.foldr (fun a b g => f g a b) acc) init := by
|
||||
simp only [Raw.foldRev, Raw.foldRevM, ← Array.foldrM_toList, Array.foldr_toList,
|
||||
← List.foldr_eq_foldrM, Id.run, AssocList.foldr]
|
||||
|
||||
theorem foldRev_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
|
||||
l.foldRev (fun acc k v => f k v :: acc) acc =
|
||||
((toListModel l.buckets).map (fun p => f p.1 p.2)) ++ acc := by
|
||||
rw [foldRev_eq, ← Array.foldr_toList, toListModel]
|
||||
generalize l.buckets.toList = l
|
||||
induction l generalizing acc with
|
||||
| nil => simp
|
||||
| cons x xs ih =>
|
||||
rw [foldr_cons, ih, AssocList.foldr_apply]
|
||||
simp
|
||||
|
||||
theorem foldRev_cons {l : Raw α β} {acc : List ((a : α) × β a)} :
|
||||
l.foldRev (fun acc k v => ⟨k, v⟩ :: acc) acc = toListModel l.buckets ++ acc := by
|
||||
simp [foldRev_cons_apply]
|
||||
|
||||
theorem foldRev_cons_key {l : Raw α β} {acc : List α} :
|
||||
l.foldRev (fun acc k _ => k :: acc) acc = List.keys (toListModel l.buckets) ++ acc := by
|
||||
rw [foldRev_cons_apply, keys_eq_map]
|
||||
|
||||
theorem toList_perm_toListModel {m : Raw α β} : Perm m.toList (toListModel m.buckets) := by
|
||||
simp [Raw.toList, fold_cons]
|
||||
simp [Raw.toList, foldRev_cons]
|
||||
|
||||
theorem keys_perm_keys_toListModel {m : Raw α β} :
|
||||
Perm m.keys (List.keys (toListModel m.buckets)) := by
|
||||
simp [Raw.keys, fold_cons_key, keys_eq_map]
|
||||
simp [Raw.keys, foldRev_cons_key, keys_eq_map]
|
||||
|
||||
theorem length_keys_eq_length_keys {m : Raw α β} :
|
||||
m.keys.length = (List.keys (toListModel m.buckets)).length :=
|
||||
|
|
|
|||
|
|
@ -333,6 +333,19 @@ map in some order.
|
|||
@[inline] def fold (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ :=
|
||||
Id.run (b.foldM f init)
|
||||
|
||||
/--
|
||||
Monadically computes a value by folding the given function over the mappings in the hash
|
||||
map in the reverse order used by `foldM`.
|
||||
-/
|
||||
@[inline] def foldRevM (f : δ → (a : α) → β a → m δ) (init : δ) (b : Raw α β) : m δ :=
|
||||
b.buckets.foldrM (fun l acc => l.foldrM (fun a b d => f d a b) acc) init
|
||||
|
||||
/--
|
||||
Folds the given function over the mappings in the hash map in the reverse order used
|
||||
by `foldM`. -/
|
||||
@[inline] def foldRev (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ :=
|
||||
Id.run (b.foldRevM f init)
|
||||
|
||||
/-- Carries out a monadic action on each mapping in the hash map in some order. -/
|
||||
@[inline] def forM (f : (a : α) → β a → m PUnit) (b : Raw α β) : m PUnit :=
|
||||
b.buckets.forM (AssocList.forM f)
|
||||
|
|
@ -349,7 +362,7 @@ instance : ForIn m (Raw α β) ((a : α) × β a) where
|
|||
|
||||
/-- Transforms the hash map into a list of mappings in some order. -/
|
||||
@[inline] def toList (m : Raw α β) : List ((a : α) × β a) :=
|
||||
m.fold (fun acc k v => ⟨k, v⟩ :: acc) []
|
||||
m.foldRev (fun acc k v => ⟨k, v⟩ :: acc) []
|
||||
|
||||
/-- Transforms the hash map into an array of mappings in some order. -/
|
||||
@[inline] def toArray (m : Raw α β) : Array ((a : α) × β a) :=
|
||||
|
|
@ -357,7 +370,7 @@ instance : ForIn m (Raw α β) ((a : α) × β a) where
|
|||
|
||||
@[inline, inherit_doc Raw.toList] def Const.toList {β : Type v} (m : Raw α (fun _ => β)) :
|
||||
List (α × β) :=
|
||||
m.fold (fun acc k v => ⟨k, v⟩ :: acc) []
|
||||
m.foldRev (fun acc k v => ⟨k, v⟩ :: acc) []
|
||||
|
||||
@[inline, inherit_doc Raw.toArray] def Const.toArray {β : Type v} (m : Raw α (fun _ => β)) :
|
||||
Array (α × β) :=
|
||||
|
|
@ -369,7 +382,7 @@ instance : ForIn m (Raw α β) ((a : α) × β a) where
|
|||
|
||||
/-- Returns a list of all values present in the hash map in some order. -/
|
||||
@[inline] def values {β : Type v} (m : Raw α (fun _ => β)) : List β :=
|
||||
m.fold (fun acc _ v => v :: acc) []
|
||||
m.foldRev (fun acc _ v => v :: acc) []
|
||||
|
||||
/-- Returns an array of all values present in the hash map in some order. -/
|
||||
@[inline] def valuesArray {β : Type v} (m : Raw α (fun _ => β)) : Array β :=
|
||||
|
|
@ -455,7 +468,7 @@ end Unverified
|
|||
|
||||
/-- Returns a list of all keys present in the hash map in some order. -/
|
||||
@[inline] def keys (m : Raw α β) : List α :=
|
||||
m.fold (fun acc k _ => k :: acc) []
|
||||
m.foldRev (fun acc k _ => k :: acc) []
|
||||
|
||||
section WF
|
||||
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ def m : DHashMap.Raw Nat (fun _ => Nat) :=
|
|||
#guard_msgs in
|
||||
#eval (m.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList
|
||||
|
||||
/-- info: [⟨3, none⟩, ⟨2, some 8⟩, ⟨1, none⟩] -/
|
||||
/-- info: [⟨1, none⟩, ⟨2, some 8⟩, ⟨3, none⟩] -/
|
||||
#guard_msgs in
|
||||
#eval (m.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList
|
||||
|
||||
|
|
@ -50,7 +50,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
ans := (k, v) :: ans
|
||||
return ans
|
||||
|
||||
/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩] -/
|
||||
/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
|
||||
#guard_msgs in
|
||||
#eval m.toList
|
||||
|
||||
|
|
@ -58,7 +58,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.toArray
|
||||
|
||||
/-- info: [(3, 6), (2, 4), (1, 2)] -/
|
||||
/-- info: [(1, 2), (2, 4), (3, 6)] -/
|
||||
#guard_msgs in
|
||||
#eval DHashMap.Raw.Const.toList m
|
||||
|
||||
|
|
@ -66,7 +66,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval DHashMap.Raw.Const.toArray m
|
||||
|
||||
/-- info: [3, 2, 1] -/
|
||||
/-- info: [1, 2, 3] -/
|
||||
#guard_msgs in
|
||||
#eval m.keys
|
||||
|
||||
|
|
@ -74,19 +74,19 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.keysArray
|
||||
|
||||
/-- info: [6, 4, 2] -/
|
||||
/-- info: [2, 4, 6] -/
|
||||
#guard_msgs in
|
||||
#eval m.values
|
||||
|
||||
/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩, ⟨16, 9⟩] -/
|
||||
/-- info: [⟨16, 9⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
|
||||
#guard_msgs in
|
||||
#eval (m.insertMany [⟨16, 8⟩, ⟨16, 9⟩]).toList
|
||||
|
||||
/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩, ⟨16, 9⟩] -/
|
||||
/-- info: [⟨16, 9⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
|
||||
#guard_msgs in
|
||||
#eval (DHashMap.Raw.Const.insertMany m [(16, 8), (16, 9)]).toList
|
||||
|
||||
/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩] -/
|
||||
/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
|
||||
#guard_msgs in
|
||||
#eval (DHashMap.Raw.Const.ofList [(1, 2), (2, 4), (3, 6)]).toList
|
||||
|
||||
|
|
@ -105,7 +105,7 @@ def m : DHashMap Nat (fun _ => Nat) :=
|
|||
#guard_msgs in
|
||||
#eval (m.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList
|
||||
|
||||
/-- info: [⟨3, none⟩, ⟨2, some 8⟩, ⟨1, none⟩] -/
|
||||
/-- info: [⟨1, none⟩, ⟨2, some 8⟩, ⟨3, none⟩] -/
|
||||
#guard_msgs in
|
||||
#eval (m.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList
|
||||
|
||||
|
|
@ -140,7 +140,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
ans := (k, v) :: ans
|
||||
return ans
|
||||
|
||||
/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩] -/
|
||||
/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
|
||||
#guard_msgs in
|
||||
#eval m.toList
|
||||
|
||||
|
|
@ -148,7 +148,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.toArray
|
||||
|
||||
/-- info: [(3, 6), (2, 4), (1, 2)] -/
|
||||
/-- info: [(1, 2), (2, 4), (3, 6)] -/
|
||||
#guard_msgs in
|
||||
#eval DHashMap.Const.toList m
|
||||
|
||||
|
|
@ -156,7 +156,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval DHashMap.Const.toArray m
|
||||
|
||||
/-- info: [3, 2, 1] -/
|
||||
/-- info: [1, 2, 3] -/
|
||||
#guard_msgs in
|
||||
#eval m.keys
|
||||
|
||||
|
|
@ -164,19 +164,19 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.keysArray
|
||||
|
||||
/-- info: [6, 4, 2] -/
|
||||
/-- info: [2, 4, 6] -/
|
||||
#guard_msgs in
|
||||
#eval m.values
|
||||
|
||||
/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩, ⟨16, 9⟩] -/
|
||||
/-- info: [⟨16, 9⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
|
||||
#guard_msgs in
|
||||
#eval (m.insertMany [⟨16, 8⟩, ⟨16, 9⟩]).toList
|
||||
|
||||
/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩, ⟨16, 9⟩] -/
|
||||
/-- info: [⟨16, 9⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
|
||||
#guard_msgs in
|
||||
#eval (DHashMap.Const.insertMany m [(16, 8), (16, 9)]).toList
|
||||
|
||||
/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩] -/
|
||||
/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/
|
||||
#guard_msgs in
|
||||
#eval (DHashMap.Const.ofList [(1, 2), (2, 4), (3, 6)]).toList
|
||||
|
||||
|
|
@ -195,7 +195,7 @@ def m : HashMap.Raw Nat Nat :=
|
|||
#guard_msgs in
|
||||
#eval (m.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList
|
||||
|
||||
/-- info: [(3, none), (2, some 8), (1, none)] -/
|
||||
/-- info: [(1, none), (2, some 8), (3, none)] -/
|
||||
#guard_msgs in
|
||||
#eval (m.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList
|
||||
|
||||
|
|
@ -230,7 +230,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
ans := (k, v) :: ans
|
||||
return ans
|
||||
|
||||
/-- info: [(3, 6), (2, 4), (1, 2)] -/
|
||||
/-- info: [(1, 2), (2, 4), (3, 6)] -/
|
||||
#guard_msgs in
|
||||
#eval m.toList
|
||||
|
||||
|
|
@ -238,7 +238,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.toArray
|
||||
|
||||
/-- info: [3, 2, 1] -/
|
||||
/-- info: [1, 2, 3] -/
|
||||
#guard_msgs in
|
||||
#eval m.keys
|
||||
|
||||
|
|
@ -246,11 +246,11 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.keysArray
|
||||
|
||||
/-- info: [6, 4, 2] -/
|
||||
/-- info: [2, 4, 6] -/
|
||||
#guard_msgs in
|
||||
#eval m.values
|
||||
|
||||
/-- info: [(3, 6), (2, 4), (1, 2), (16, 9)] -/
|
||||
/-- info: [(16, 9), (1, 2), (2, 4), (3, 6)] -/
|
||||
#guard_msgs in
|
||||
#eval (m.insertMany [(16, 8), (16, 9)]).toList
|
||||
|
||||
|
|
@ -269,7 +269,7 @@ def m : HashMap Nat Nat :=
|
|||
#guard_msgs in
|
||||
#eval (m.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList
|
||||
|
||||
/-- info: [(3, none), (2, some 8), (1, none)] -/
|
||||
/-- info: [(1, none), (2, some 8), (3, none)] -/
|
||||
#guard_msgs in
|
||||
#eval (m.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList
|
||||
|
||||
|
|
@ -304,7 +304,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
ans := (k, v) :: ans
|
||||
return ans
|
||||
|
||||
/-- info: [(3, 6), (2, 4), (1, 2)] -/
|
||||
/-- info: [(1, 2), (2, 4), (3, 6)] -/
|
||||
#guard_msgs in
|
||||
#eval m.toList
|
||||
|
||||
|
|
@ -312,7 +312,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.toArray
|
||||
|
||||
/-- info: [3, 2, 1] -/
|
||||
/-- info: [1, 2, 3] -/
|
||||
#guard_msgs in
|
||||
#eval m.keys
|
||||
|
||||
|
|
@ -320,11 +320,11 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.keysArray
|
||||
|
||||
/-- info: [6, 4, 2] -/
|
||||
/-- info: [2, 4, 6] -/
|
||||
#guard_msgs in
|
||||
#eval m.values
|
||||
|
||||
/-- info: [(3, 6), (2, 4), (1, 2), (16, 9)] -/
|
||||
/-- info: [(16, 9), (1, 2), (2, 4), (3, 6)] -/
|
||||
#guard_msgs in
|
||||
#eval (m.insertMany [(16, 8), (16, 9)]).toList
|
||||
|
||||
|
|
@ -332,35 +332,35 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval HashMap.ofList [(1, 2), (1, 4)]
|
||||
|
||||
/-- info: Std.HashMap.ofList [(37, 37), (4, 5), (3, 6), (2, 4), (1, 2)] -/
|
||||
/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 6), (4, 5), (37, 37)] -/
|
||||
#guard_msgs in
|
||||
#eval m ∪ {(4, 5), (37, 37)}
|
||||
|
||||
/-- info: Std.HashMap.ofList [(3, 6), (2, 4), (1, 3)] -/
|
||||
/-- info: Std.HashMap.ofList [(1, 3), (2, 4), (3, 6)] -/
|
||||
#guard_msgs in
|
||||
#eval m.modify 1 (fun v => v + 1)
|
||||
|
||||
/-- info: Std.HashMap.ofList [(3, 6), (2, 4), (1, 2)] -/
|
||||
/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 6)] -/
|
||||
#guard_msgs in
|
||||
#eval m.modify 4 (fun v => v + 1)
|
||||
|
||||
/-- info: Std.HashMap.ofList [(3, 6), (2, 4), (1, 2)] -/
|
||||
/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 6)] -/
|
||||
#guard_msgs in
|
||||
#eval m.alter 4 (fun v? => v?.map (· + 2))
|
||||
|
||||
/-- info: Std.HashMap.ofList [(4, 7), (3, 6), (2, 4), (1, 2)] -/
|
||||
/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 6), (4, 7)] -/
|
||||
#guard_msgs in
|
||||
#eval m.alter 4 (fun _ => some 7)
|
||||
|
||||
/-- info: Std.HashMap.ofList [(3, 6), (2, 4), (1, 2)] -/
|
||||
/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 6)] -/
|
||||
#guard_msgs in
|
||||
#eval m.alter 4 (fun _ => none)
|
||||
|
||||
/-- info: Std.HashMap.ofList [(2, 4), (1, 2)] -/
|
||||
/-- info: Std.HashMap.ofList [(1, 2), (2, 4)] -/
|
||||
#guard_msgs in
|
||||
#eval m.alter 3 (fun _ => none)
|
||||
|
||||
/-- info: Std.HashMap.ofList [(3, 37), (2, 4), (1, 2)] -/
|
||||
/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 37)] -/
|
||||
#guard_msgs in
|
||||
#eval m.alter 3 (fun _ => some 37)
|
||||
|
||||
|
|
@ -418,7 +418,7 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.all fun x => x > 4
|
||||
|
||||
/-- info: [1000000000, 2, 1] -/
|
||||
/-- info: [1, 2, 1000000000] -/
|
||||
#guard_msgs in
|
||||
#eval m.toList
|
||||
|
||||
|
|
@ -426,15 +426,15 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.toArray
|
||||
|
||||
/-- info: Std.HashSet.Raw.ofList [1000000000, 2, 1, 16] -/
|
||||
/-- info: Std.HashSet.Raw.ofList [16, 1, 2, 1000000000] -/
|
||||
#guard_msgs in
|
||||
#eval m ∪ {16, 16}
|
||||
|
||||
/-- info: [1000000000, 2, 1, 16] -/
|
||||
/-- info: [16, 1, 2, 1000000000] -/
|
||||
#guard_msgs in
|
||||
#eval (m.insertMany [16, 16]).toList
|
||||
|
||||
/-- info: Std.HashSet.Raw.ofList [100, 1] -/
|
||||
/-- info: Std.HashSet.Raw.ofList [1, 100] -/
|
||||
#guard_msgs in
|
||||
#eval HashSet.Raw.ofList [1, 100]
|
||||
|
||||
|
|
@ -492,7 +492,7 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.all fun x => x > 4
|
||||
|
||||
/-- info: [1000000000, 2, 1] -/
|
||||
/-- info: [1, 2, 1000000000] -/
|
||||
#guard_msgs in
|
||||
#eval m.toList
|
||||
|
||||
|
|
@ -500,15 +500,15 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do
|
|||
#guard_msgs in
|
||||
#eval m.toArray
|
||||
|
||||
/-- info: Std.HashSet.ofList [1000000000, 2, 1, 16] -/
|
||||
/-- info: Std.HashSet.ofList [16, 1, 2, 1000000000] -/
|
||||
#guard_msgs in
|
||||
#eval m ∪ {16, 16}
|
||||
|
||||
/-- info: [1000000000, 2, 1, 16] -/
|
||||
/-- info: [16, 1, 2, 1000000000] -/
|
||||
#guard_msgs in
|
||||
#eval (m.insertMany [16, 16]).toList
|
||||
|
||||
/-- info: Std.HashSet.ofList [100, 1] -/
|
||||
/-- info: Std.HashSet.ofList [1, 100] -/
|
||||
#guard_msgs in
|
||||
#eval HashSet.ofList [1, 100]
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue