@@ -36,7 +36,9 @@ An \Idris{} file consists of an optional module declaration (here
36however \Idris{} programs can consist of several modules, and the definitions
36however \Idris{} programs can consist of several modules, and the definitions
37in each module each have their own namespace, as we will discuss in Section
37in each module each have their own namespace, as we will discuss in Section
38\ref{sect:namespaces}) and a
38\ref{sect:namespaces}) and a
39−collection of declarations and definitions. Each definition must have a type
39+collection of declarations and definitions. The order of definitions is
40+significant --- functions and data types must be defined before use.
41+Each definition must have a type
40declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
42declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
41Indentation is significant --- a new declaration begins at the same level
43Indentation is significant --- a new declaration begins at the same level
42of indentation as the preceding declaration. Alternatively, declarations
44of indentation as the preceding declaration. Alternatively, declarations
@@ -245,6 +247,38 @@ foo x = case isLT of
245\end{SaveVerbatim}
247\end{SaveVerbatim}
246\useverb{wheredata}
248\useverb{wheredata}
251+In general, functions defined in a \texttt{where} clause need a type declaration
252+just like any top level function. However, the type declaration for
253+a function \texttt{f} \remph{can} be omitted if:
256+\item \texttt{f} appears in the right hand side of the top level definition
257+\item The type of \texttt{f} can be completely determined from its first
262+So, for example, the following definitions are legal:
264+\begin{SaveVerbatim}{whereinfer}
268+even (S k) = odd k where
272+test : Num a => List a
273+test = [c 1, c 2, d 3]
275+ d y = c (y + 1 + z y)
248\subsection{Dependent Types}
282\subsection{Dependent Types}
250\subsubsection{Vectors}
284\subsubsection{Vectors}
@@ -486,6 +520,33 @@ using (x:a, y:a, xs:Vect a n)
486\end{SaveVerbatim}
520\end{SaveVerbatim}
487\useverb{elemusing}
521\useverb{elemusing}
523+\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}
525+In general, functions and data types must be defined before use, since
526+dependent types allow functions to appear as part of types, and their
527+reduction behaviour to affect type checking. However, this
528+restriction can be relaxed by using a \texttt{mutual} block, which allows
529+data types and functions to be defined simultaneously:
531+\begin{SaveVerbatim}{mutual}
546+In a \texttt{mutual} block, first all of the type declarations are added,
547+then the function bodies. As a result, none of the function types can depend
548+on the reduction behaviour of any of the functions in the block.
489\subsection{I/O}
550\subsection{I/O}
491Computer programs are of little use if they do not interact with the user or
552Computer programs are of little use if they do not interact with the user or