@@ -10,11 +10,11 @@ module, a list of ``import`` statements giving the other modules which
10are to be imported, and a collection of declarations and definitions of
10are to be imported, and a collection of declarations and definitions of
11types, classes and functions. For example, the listing below gives a
11types, classes and functions. For example, the listing below gives a
12module which defines a binary tree type ``BTree`` (in a file
12module which defines a binary tree type ``BTree`` (in a file
13−``btree.idr``):
13+``Btree.idr``):
15.. code-block:: idris
15.. code-block:: idris
17− module btree
17+ module Btree
19 data BTree a = Leaf
19 data BTree a = Leaf
20 | Node (BTree a) a (BTree a)
20 | Node (BTree a) a (BTree a)
@@ -40,23 +40,24 @@ Then, this gives a main program (in a file
41 module Main
41 module Main
43− import btree
43+ import Btree
45 main : IO ()
45 main : IO ()
46 main = do let t = toTree [1,8,2,7,9,3]
46 main = do let t = toTree [1,8,2,7,9,3]
47 print (btree.toList t)
47 print (btree.toList t)
50The same names can be defined in multiple modules. This is possible
51The same names can be defined in multiple modules. This is possible
51because in practice names are *qualified* with the name of the module.
52because in practice names are *qualified* with the name of the module.
52The names defined in the ``btree`` module are, in full:
53The names defined in the ``btree`` module are, in full:
54−+ ``btree.BTree``
55++ ``Btree.BTree``
55−+ ``btree.Leaf``
56++ ``Btree.Leaf``
56−+ ``btree.Node``
57++ ``Btree.Node``
57−+ ``btree.insert``
58++ ``Btree.insert``
58−+ ``btree.toList``
59++ ``Btree.toList``
59−+ ``btree.toTree``
60++ ``Btree.toTree``
61If names are otherwise unambiguous, there is no need to give the fully
62If names are otherwise unambiguous, there is no need to give the fully
62qualified name. Names can be disambiguated either by giving an explicit
63qualified name. Names can be disambiguated either by giving an explicit
@@ -103,7 +104,7 @@ functions to be exported as ``abstract``, as we see below:
104.. code-block:: idris
105.. code-block:: idris
106− module btree
107+ module Btree
108 abstract data BTree a = Leaf
109 abstract data BTree a = Leaf
109 | Node (BTree a) a (BTree a)
110 | Node (BTree a) a (BTree a)
@@ -137,7 +138,8 @@ the ``public`` modifier on an ``import``. For example:
140− import B import public C
142+ import public C
142 public a : AType a = ...
144 public a : AType a = ...
@@ -154,7 +156,7 @@ wish to overload names within the same module:
155.. code-block:: idris
157.. code-block:: idris
157− module foo
159+ module Foo
159 namespace x
161 namespace x
160 test : Int -> Int
162 test : Int -> Int