@@ -36,7 +36,9 @@ An \Idris{} file consists of an optional module declaration (here
3636however \Idris{} programs can consist of several modules, and the definitions
3737in each module each have their own namespace, as we will discuss in Section
3838\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
4042declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
4143Indentation is significant --- a new declaration begins at the same level
4244of indentation as the preceding declaration. Alternatively, declarations
@@ -245,6 +247,38 @@ foo x = case isLT of
245247\end{SaveVerbatim}
246248\useverb{wheredata}
247249
250+\noindent
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:
254+
255+\begin{itemize}
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
258+application
259+\end{itemize}
260+
261+\noindent
262+So, for example, the following definitions are legal:
263+
264+\begin{SaveVerbatim}{whereinfer}
265+
266+even : Nat -> Bool
267+even O = True
268+even (S k) = odd k where
269+ odd O = False
270+ odd (S k) = even k
271+
272+test : Num a => List a
273+test = [c 1, c 2, d 3]
274+ where c x = 42 + x
275+ d y = c (y + 1 + z y)
276+ where z w = y + w
277+
278+\end{SaveVerbatim}
279+\useverb{whereinfer}
280+
281+
248282\subsection{Dependent Types}
249283
250284\subsubsection{Vectors}
@@ -486,6 +520,33 @@ using (x:a, y:a, xs:Vect a n)
486520\end{SaveVerbatim}
487521\useverb{elemusing}
488522
523+\subsubsection*{Note: Declaration Order and \texttt{mutual} blocks}
524+
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:
530+
531+\begin{SaveVerbatim}{mutual}
532+
533+mutual
534+ even : Nat -> Bool
535+ even O = True
536+ even (S k) = odd k
537+
538+ odd : Nat -> Bool
539+ odd O = False
540+ odd (S k) = even k
541+
542+\end{SaveVerbatim}
543+\useverb{mutual}
544+
545+\noindent
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.
549+
489550\subsection{I/O}
490551
491552Computer programs are of little use if they do not interact with the user or