Added AVL.Map suggestion, explanation of MkValue args. (#2447)

* Added AVL.Map suggestion, explanation of MkValue args.

* Added AVL.Map suggestion, explanation of MkValue args.

* Added backticks, other formatting, clarified (Vec String) as function.

As suggested by @MatthewDaggit.

I also lowercased the initial letter after colon in third new
paragraph.

---------

Co-authored-by: Marshall Abrams <[email protected]>

Author: mars0i

doc/README/Data/Tree/AVL.agda

@@ -28,6 +28,21 @@ open import Relation.Binary.PropositionalEquality
 open Data.Tree.AVL <-strictTotalOrder renaming (Tree to Tree′)
 Tree = Tree′ (MkValue (Vec String) (subst (Vec String)))
 
+-- The first argument to `MkValue` should be a function from a key
+-- (a `ℕ` in this case) to a value type (a `String` vector type).
+-- Since `(Vec String)` is missing `Vec`'s second parameter, a `ℕ`,
+-- it's equivalent to `λ n → Vec String n`.
+
+-- The second argument to `MkValue` is a function that can accept
+-- a proof that two keys are equal, and then substitute a unique key
+-- for an equivalent key that is passed in.  Applying `subst` to the
+-- key-to-value-type function passed as `MkValue`'s first argument is
+-- a normal way to create such a function.
+
+-- Note that there is no need to define the type of keys separately:
+-- passing a key-to-value-type function to `MkValue` and providing
+-- the result of `MkValue` to `Data.Tree.AVL.Tree` is enough.
+
 ------------------------------------------------------------------------
 -- Construction of trees
 
@@ -127,6 +142,10 @@ v₉ = refl
 
 -- Variations of the AVL tree module are available:
 
+-- • Finite maps in which types of values don't depend on keys.
+
+import Data.Tree.AVL.Map
+
 -- • Finite maps with indexed keys and values.
 
 import Data.Tree.AVL.IndexedMap