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 ecf687b commit 25a2051Copy full SHA for 25a2051
src/Std/Data/DTreeMap/Internal/Operations.lean
@@ -518,7 +518,7 @@ abbrev IteratedSlowNewInsertionInto [Ord α] (t) :=
518
{ t' // ∀ {P : Impl α β → Prop}, P t → (∀ t'' a b, P t'' → P (t''.insertIfNew! a b)) → P t' }
519
520
/--
521
-Computes the union of the given tree maps. If a key appears in both maps, the entry contains in the second argument will appear in the result.
+Computes the union of the given tree maps. If a key appears in both maps, the entry contained in the second argument will appear in the result.
522
523
This function always merges the smaller map into the larger map.
524
-/
0 commit comments