We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 65a8dfb commit 76328c7Copy full SHA for 76328c7
src/Std/Data/DTreeMap/Basic.lean
@@ -1075,7 +1075,7 @@ def insertMany {ρ} [ForIn Id ρ ((a : α) × β a)] (t : DTreeMap α β cmp) (l
1075
1076
/--
1077
Inserts multiple mappings into the tree map by iterating over the given collection and calling
1078
-`insert`. If the same key appears multiple times, the first occurrence takes precedence.
+`insertIfNew`. If the same key appears multiple times, the first occurrence takes precedence.
1079
-/
1080
@[inline]
1081
def insertManyIfNew {ρ} [ForIn Id ρ ((a : α) × β a)] (t : DTreeMap α β cmp) (l : ρ) : DTreeMap α β cmp :=
0 commit comments