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