    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Some examples showing how the AVL tree module can be used
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module README.Data.Tree.AVL where

    ------------------------------------------------------------------------
    -- Setup

    -- AVL trees are defined in Data.Tree.AVL.

    import Data.Tree.AVL

    -- This module is parametrised by keys, which have to form a (strict)
    -- total order, and values, which are indexed by keys. Let us use
    -- natural numbers as keys and vectors of strings as values.

    open import Data.Nat.Properties using (<-strictTotalOrder)
    open import Data.Product.Base as Product using (_,_; _,′_)
    open import Data.String.Base using (String)
    open import Data.Vec.Base using (Vec; _∷_; [])
    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

    -- Some values.

    v₁  = "cepa" ∷ []
    v₁′ = "depa" ∷ []
    v₂  = "apa" ∷ "bepa" ∷ []

    -- Empty and singleton trees.

    t₀ : Tree
    t₀ = empty

    t₁ : Tree
    t₁ = singleton 2 v₂

    -- Insertion of a key-value pair into a tree.

    t₂ = insert 1 v₁ t₁

    -- If you insert a key-value pair and the key already exists in the
    -- tree, then the old value is thrown away.

    t₂′ = insert 1 v₁′ t₂

    -- Deletion of the mapping for a certain key.

    t₃ = delete 2 t₂

    -- Conversion of a list of key-value mappings to a tree.

    open import Data.List.Base using (_∷_; [])

    t₄ : Tree
    t₄ = fromList ((2 , v₂) ∷ (1 , v₁) ∷ [])

    ------------------------------------------------------------------------
    -- Queries

    -- Let us formulate queries as unit tests.

    open import Relation.Binary.PropositionalEquality using (_≡_; refl)

    -- Searching for a key.

    open import Data.Bool.Base using (true; false)
    open import Data.Maybe.Base as Maybe using (just; nothing)

    q₀ : lookup t₂ 2 ≡ just v₂
    q₀ = refl

    q₁ : lookup t₃ 2 ≡ nothing
    q₁ = refl

    q₂ : (3 ∈? t₂) ≡ false
    q₂ = refl

    q₃ : (1 ∈? t₄) ≡ true
    q₃ = refl

    -- Turning a tree into a sorted list of key-value pairs.

    q₄ : toList t₁ ≡ (2 , v₂) ∷ []
    q₄ = refl

    q₅ : toList t₂ ≡ (1 , v₁) ∷ (2 , v₂) ∷ []
    q₅ = refl

    q₅′ : toList t₂′ ≡ (1 , v₁′) ∷ (2 , v₂) ∷ []
    q₅′ = refl

    ------------------------------------------------------------------------
    -- Views

    -- Partitioning a tree into the smallest element plus the rest, or the
    -- largest element plus the rest.

    open import Function.Base using (id)

    v₆ : headTail t₀ ≡ nothing
    v₆ = refl

    v₇ : Maybe.map (Product.map₂ toList) (headTail t₂) ≡
         just ((1 , v₁) , ((2 , v₂) ∷ []))
    v₇ = refl

    v₈ : initLast t₀ ≡ nothing
    v₈ = refl

    v₉ : Maybe.map (Product.map₁ toList) (initLast t₄) ≡
         just (((1 , v₁) ∷ []) ,′ (2 , v₂))
    v₉ = refl

    ------------------------------------------------------------------------
    -- Further reading

    -- 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

    -- • Finite sets.

    import Data.Tree.AVL.Sets