docs

Author: Rob23oba

src/Std/Data/DTreeMap/Lemmas.lean

@@ -11,7 +11,7 @@ import Std.Data.DTreeMap.AdditionalOperations
 /-!
 # Dependent tree map lemmas
 
-This file contains lemmas about `Std.Data.DTreeMap`. Most of the lemmas require
+This file contains lemmas about `Std.DTreeMap`. Most of the lemmas require
 `TransCmp cmp` for the comparison function `cmp`.
 -/
 

src/Std/Data/ExtDTreeMap/Basic.lean

@@ -59,7 +59,7 @@ Internally, the tree maps are represented as size-bounded trees, a type of self-
 search tree with efficient order statistic lookups.
 
 In contrast to regular dependent tree maps, `Std.ExtDTreeMap` offers several extensionality lemmas
-and therefore has more lemmas about equality of tree maps This doesn't affect the amount of
+and therefore has more lemmas about equality of tree maps. This doesn't affect the amount of
 supported functions though: `Std.ExtDTreeMap` supports all operations from `Std.DTreeMap`.
 
 In order to use most functions, a `TransCmp` instance is required. This is necessary to make sure

src/Std/Data/ExtDTreeMap/Lemmas.lean

@@ -9,7 +9,7 @@ import Std.Data.ExtDTreeMap.Basic
 /-!
 # Extensional dependent tree map lemmas
 
-This file contains lemmas about `Std.Data.ExtDTreeMap`.
+This file contains lemmas about `Std.ExtDTreeMap`.
 -/
 
 set_option linter.missingDocs true

src/Std/Data/ExtTreeMap/Basic.lean

@@ -28,7 +28,7 @@ variable {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering
 namespace Std
 
 /--
-Tree maps.
+Extensional tree maps.
 
 A tree map stores an assignment of keys to values. It depends on a comparator function that
 defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval
@@ -51,6 +51,14 @@ To avoid expensive copies, users should make sure that the tree map is used line
 Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary
 search tree with efficient order statistic lookups.
 
+In contrast to regular tree maps, `Std.ExtTreeMap` offers several extensionality lemmas
+and therefore has more lemmas about equality of tree maps. This doesn't affect the amount of
+supported functions though: `Std.ExtTreeMap` supports all operations from `Std.TreeMap`.
+
+In order to use most functions, a `TransCmp` instance is required. This is necessary to make sure
+that the functions are congruent, i.e. equivalent tree maps as parameters produce equivalent return
+values.
+
 These tree maps contain a bundled well-formedness invariant, which means that they cannot
 be used in nested inductive types. For these use cases, `Std.TreeMap.Raw` and
 `Std.TreeMap.Raw.WF` unbundle the invariant from the tree map. When in doubt, prefer

src/Std/Data/ExtTreeMap/Lemmas.lean

@@ -10,8 +10,7 @@ import Std.Data.ExtTreeMap.Basic
 /-!
 # Extensional tree map lemmas
 
-This file contains lemmas about `Std.Data.ExtTreeMap`. Most of the lemmas require
-`TransCmp cmp` for the comparison function `cmp`.
+This file contains lemmas about `Std.ExtTreeMap`.
 -/
 
 set_option linter.missingDocs true

src/Std/Data/ExtTreeSet/Basic.lean

@@ -28,7 +28,7 @@ variable {α : Type u} {cmp : α → α → Ordering}
 namespace Std
 
 /--
-Tree sets.
+Extensional tree sets.
 
 A tree set stores elements of a certain type in a certain order. It depends on a comparator function
 that defines an ordering on the keys and provides efficient order-dependent queries, such as
@@ -50,6 +50,14 @@ To avoid expensive copies, users should make sure that the tree set is used line
 Internally, the tree sets are represented as size-bounded trees, a type of self-balancing binary
 search tree with efficient order statistic lookups.
 
+In contrast to regular dependent tree maps, `Std.ExtTreeSet` offers several extensionality lemmas
+and therefore has more lemmas about equality of tree sets. This doesn't affect the amount of
+supported functions though: `Std.ExtTreeSet` supports all operations from `Std.TreeMap`.
+
+In order to use most functions, a `TransCmp` instance is required. This is necessary to make sure
+that the functions are congruent, i.e. equivalent tree sets as parameters produce equivalent return
+values.
+
 These tree sets contain a bundled well-formedness invariant, which means that they cannot
 be used in nested inductive types. For these use cases, `Std.TreeSet.Raw` and
 `Std.TreeSet.Raw.WF` unbundle the invariant from the tree set. When in doubt, prefer

src/Std/Data/ExtTreeSet/Lemmas.lean

@@ -10,8 +10,7 @@ import Std.Data.ExtTreeSet.Basic
 /-!
 # Tree set lemmas
 
-This file contains lemmas about `Std.Data.ExtTreeSet`. Most of the lemmas require
-`TransCmp cmp` for the comparison function `cmp`.
+This file contains lemmas about `Std.ExtTreeSet`.
 -/
 
 set_option linter.missingDocs true

src/Std/Data/TreeMap/Basic.lean

@@ -15,7 +15,7 @@ Lemmas about the operations on `Std.TreeMap` will be available in the
 module `Std.Data.TreeMap.Lemmas`.
 
 See the module `Std.Data.TreeMap.Raw.Basic` for a variant of this type which is safe to use in
-nested inductive types.
+nested inductive types and `Std.Data.ExtTreeMap.Basic` for a variant with extensionality.
 -/
 
 set_option autoImplicit false
@@ -51,6 +51,10 @@ To avoid expensive copies, users should make sure that the tree map is used line
 Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary
 search tree with efficient order statistic lookups.
 
+For use in proofs, the type `Std.ExtTreeMap` of extensional tree maps should be preferred. This
+type comes with several extensionality lemmas and provides the same functions but requires a
+`TransCmp` instance to work with.
+
 These tree maps contain a bundled well-formedness invariant, which means that they cannot
 be used in nested inductive types. For these use cases, `Std.TreeMap.Raw` and
 `Std.TreeMap.Raw.WF` unbundle the invariant from the tree map. When in doubt, prefer

src/Std/Data/TreeMap/Lemmas.lean

@@ -11,7 +11,7 @@ import Std.Data.TreeMap.AdditionalOperations
 /-!
 # Tree map lemmas
 
-This file contains lemmas about `Std.Data.TreeMap`. Most of the lemmas require
+This file contains lemmas about `Std.TreeMap`. Most of the lemmas require
 `TransCmp cmp` for the comparison function `cmp`.
 -/
 

src/Std/Data/TreeSet/Basic.lean

@@ -15,7 +15,7 @@ Lemmas about the operations on `Std.Data.TreeSet` will be available in the
 module `Std.Data.TreeSet.Lemmas`.
 
 See the module `Std.Data.TreeSet.Raw.Basic` for a variant of this type which is safe to use in
-nested inductive types.
+nested inductive types and `Std.Data.ExtTreeSet.Basic` for a variant with extensionality.
 -/
 
 set_option autoImplicit false
@@ -50,6 +50,10 @@ To avoid expensive copies, users should make sure that the tree set is used line
 Internally, the tree sets are represented as size-bounded trees, a type of self-balancing binary
 search tree with efficient order statistic lookups.
 
+For use in proofs, the type `Std.ExtTreeSet` of extensional tree sets should be preferred. This
+type comes with several extensionality lemmas and provides the same functions but requires a
+`TransCmp` instance to work with.
+
 These tree sets contain a bundled well-formedness invariant, which means that they cannot
 be used in nested inductive types. For these use cases, `Std.TreeSet.Raw` and
 `Std.TreeSet.Raw.WF` unbundle the invariant from the tree set. When in doubt, prefer