@@ -10,11 +10,11 @@ module, a list of ``import`` statements giving the other modules which
1010are to be imported, and a collection of declarations and definitions of
1111types, classes and functions. For example, the listing below gives a
1212module which defines a binary tree type ``BTree`` (in a file
13−``btree.idr``):
13+``Btree.idr``):
1414
1515.. code-block:: idris
1616
17− module btree
17+ module Btree
1818
1919 data BTree a = Leaf
2020 | Node (BTree a) a (BTree a)
@@ -40,23 +40,24 @@ Then, this gives a main program (in a file
4040
4141 module Main
4242
43− import btree
43+ import Btree
4444
4545 main : IO ()
4646 main = do let t = toTree [1,8,2,7,9,3]
4747 print (btree.toList t)
4848
4949
50+
5051The same names can be defined in multiple modules. This is possible
5152because in practice names are *qualified* with the name of the module.
5253The names defined in the ``btree`` module are, in full:
5354
54−+ ``btree.BTree``
55−+ ``btree.Leaf``
56−+ ``btree.Node``
57−+ ``btree.insert``
58−+ ``btree.toList``
59−+ ``btree.toTree``
55++ ``Btree.BTree``
56++ ``Btree.Leaf``
57++ ``Btree.Node``
58++ ``Btree.insert``
59++ ``Btree.toList``
60++ ``Btree.toTree``
6061
6162If names are otherwise unambiguous, there is no need to give the fully
6263qualified name. Names can be disambiguated either by giving an explicit
@@ -103,7 +104,7 @@ functions to be exported as ``abstract``, as we see below:
103104
104105.. code-block:: idris
105106
106− module btree
107+ module Btree
107108
108109 abstract data BTree a = Leaf
109110 | Node (BTree a) a (BTree a)
@@ -137,7 +138,8 @@ the ``public`` modifier on an ``import``. For example:
137138
138139 module A
139140
140− import B import public C
141+ import B
142+ import public C
141143
142144 public a : AType a = ...
143145
@@ -154,7 +156,7 @@ wish to overload names within the same module:
154156
155157.. code-block:: idris
156158
157− module foo
159+ module Foo
158160
159161 namespace x
160162 test : Int -> Int