@@ -34,7 +34,7 @@ module which defines a binary tree type ``BTree`` (in a file
36Then, this gives a main program (in a file
36Then, this gives a main program (in a file
37−``bmain.idr``) which uses the ``bst`` module to sort a list:
37+``bmain.idr``) which uses the ``Btree`` module to sort a list:
39.. code-block:: idris
39.. code-block:: idris
@@ -50,7 +50,7 @@ Then, this gives a main program (in a file
51The same names can be defined in multiple modules. This is possible
51The same names can be defined in multiple modules. This is possible
52because in practice names are *qualified* with the name of the module.
52because in practice names are *qualified* with the name of the module.
53−The names defined in the ``btree`` module are, in full:
53+The names defined in the ``Btree`` module are, in full:
55+ ``Btree.BTree``
55+ ``Btree.BTree``
56+ ``Btree.Leaf``
56+ ``Btree.Leaf``
@@ -99,7 +99,7 @@ and classes to be marked as: ``public``, ``abstract`` or ``private``:
100 If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.
100 If any definition is given an export modifier, then all names with no modifier are assumed to be ``private``.
102−For our ``btree`` module, it makes sense for the tree data type and the
102+For our ``Btree`` module, it makes sense for the tree data type and the
103functions to be exported as ``abstract``, as we see below:
103functions to be exported as ``abstract``, as we see below:
105.. code-block:: idris
105.. code-block:: idris