@@ -35,7 +35,7 @@ toTree (x :: xs) = insert x (toTree xs)
36\begin{SaveVerbatim}{bstmain}
36\begin{SaveVerbatim}{bstmain}
38−module main
38+module Main
40import btree
40import btree
@@ -61,13 +61,14 @@ If names are otherwise unambiguous, there is no need to give the fully qualified
61Names can be disambiguated either by giving an explicit qualification, or according to
61Names can be disambiguated either by giving an explicit qualification, or according to
62their type.
62their type.
64−There is no formal link between the module name and its filename, although it is generally
64+There is no formal link between the module name and its filename, although it
65−advisable to use the same name for each. An \texttt{import} statement refers to a filename,
65+is generally advisable to use the same name for each. An \texttt{import}
66+statement refers to a filename, using dots to separate directories. For
66−using dots to separate directories. For example, \texttt{import foo.bar} would import
67+example, \texttt{import foo.bar} would import the file \texttt{foo/bar.idr},
67−the file \texttt{foo/bar.idr}, which would conventionally have the module declaration
68+which would conventionally have the module declaration \texttt{module foo.bar}.
68−\texttt{module foo.bar}. The only requirement for module names is that the main module, with
69+The only requirement for module names is that the main module, with the
69−the \texttt{main} function, must be called \texttt{main} (though its filename need not be
70+\texttt{main} function, must be called \texttt{Main} (though its filename need
70−\texttt{main.idr}).
71+not be \texttt{Main.idr}).
72\subsection{Export Modifiers}
73\subsection{Export Modifiers}