@@ -200,33 +200,6 @@ rev xs = revAcc [] xs where {
200200Any names which are visible in the outer scope are also visible in the \texttt{where}
201201clause (unless they have been redefined, such as \texttt{xs} here).
202202
203−\subsubsection*{\texttt{let} bindings}
204−
205−Intermediate values can be calculated using \texttt{let} bindings:
206−
207−\begin{SaveVerbatim}{letb}
208−
209−mirror : List a -> List a;
210−mirror xs = let xs' = rev xs in
211− app xs xs';
212−
213−\end{SaveVerbatim}
214−\useverb{letb}
215−
216−\noindent
217−We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
218−fields from a record as follows, as well as by pattern matching at the top level:
219−
220−\begin{SaveVerbatim}{letp}
221−
222−data Person = MkPerson String Int;
223−
224−showPerson : Person -> String;
225−showPerson p = let MkPerson name age = p in
226− name ++ " is " ++ show age ++ " years old";
227−
228−\end{SaveVerbatim}
229−\useverb{letp}
230203
231204\subsection{Dependent Types}
232205
@@ -294,9 +267,11 @@ app (x :: xs) ys = x :: app xs xs; -- BROKEN
294267$ idris vbroken.idr --check
295268vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m))
296269
270+\end{SaveVerbatim}
271+\begin{SaveVerbatim}{bleh}
272+$
297273\end{SaveVerbatim}
298274\useverb{vapperrmsg}
299−%$
300275
301276This error message suggests that there is a length mismatch between two vectors
302277--- we needed a vector of length \texttt{(S (k + m))}, but provided a vector
@@ -699,8 +674,8 @@ bounds error:
699674
700675list_lookup : Nat -> List a -> Maybe a;
701676list_lookup _ Nil = Nothing;
702−list_lookup O (Cons x xs) = Just x;
703−list_lookup (S k) (Cons x xs) = list_lookup k xs;
677+list_lookup O (x :: xs) = Just x;
678+list_lookup (S k) (x :: xs) = list_lookup k xs;
704679
705680\end{SaveVerbatim}
706681\useverb{lookuplist}
@@ -839,3 +814,98 @@ filter p (x :: xs) with filter p xs {
839814\noindent
840815We will see more on \texttt{with} notation later.
841816
817+\subsection{More Expressions}
818+
819+\subsubsection*{\texttt{let} bindings}
820+
821+Intermediate values can be calculated using \texttt{let} bindings:
822+
823+\begin{SaveVerbatim}{letb}
824+
825+mirror : List a -> List a;
826+mirror xs = let xs' = rev xs in
827+ app xs xs';
828+
829+\end{SaveVerbatim}
830+\useverb{letb}
831+
832+\noindent
833+We can do simple pattern matching in \texttt{let} bindings too. For example, we can extract
834+fields from a record as follows, as well as by pattern matching at the top level:
835+
836+\begin{SaveVerbatim}{letp}
837+
838+data Person = MkPerson String Int;
839+
840+showPerson : Person -> String;
841+showPerson p = let MkPerson name age = p in
842+ name ++ " is " ++ show age ++ " years old";
843+
844+\end{SaveVerbatim}
845+\useverb{letp}
846+
847+\subsubsection*{\texttt{case} expressions}
848+
849+Another way of inspecting intermediate values of \emph{simple} types
850+is to use a \texttt{case} expression.
851+The following function, for example, splits a string into two at a given character:
852+
853+\begin{SaveVerbatim}{split}
854+
855+splitAt : Char -> String -> (String, String);
856+splitAt c x = case break (== c) x of {
857+ (x, y) => (x, strTail y)
858+ };
859+
860+\end{SaveVerbatim}
861+\useverb{split}
862+
863+\noindent
864+\texttt{break} is a library function which breaks a string into a pair of strings
865+at the point where the given function is no longer true. We then deconstruct the
866+pair it returns, and remove the first character of the second string.
867+
868+A \texttt{case} expression can match several cases, for example, to inspect an
869+intermediate value of type \texttt{Maybe a}. Recall \texttt{list\_lookup} which
870+looks up an index in a list, returning \texttt{Nothing} if the index is out
871+of bounds. We can use this to write \texttt{lookup\_default}, which
872+looks up an index and returns a default value if the index is out of bounds:
873+
874+\begin{SaveVerbatim}{listlookup}
875+
876+lookup_default : Nat -> List a -> a -> a;
877+lookup_default i xs def = case list_lookup i xs of {
878+ Nothing => def
879+ | Just x => x
880+ };
881+
882+\end{SaveVerbatim}
883+\useverb{listlookup}
884+
885+\noindent
886+If the index is in bounds, we get the value at that index, otherwise we get
887+a default value:
888+
889+\begin{SaveVerbatim}{deftest}
890+
891+*usefultypes> lookup_default 2 [3,4,5,6] (-1)
892+5 : Int
893+*usefultypes> lookup_default 4 [3,4,5,6] (-1)
894+-1 : Int
895+
896+\end{SaveVerbatim}
897+\useverb{deftest}
898+
899+\noindent
900+\textbf{Restrictions:} The \texttt{case} construct is intended for simple analysis
901+of intermediate expressions to avoid the need to write auxiliary functions, and is
902+also used internally to implement pattern matching \texttt{let} and lambda bindings.
903+It will \emph{only} work if:
904+
905+\begin{itemize}
906+\item Each branch \emph{matches} a value of the same type, and \emph{returns} a
907+value of the same type.
908+\item The type of the result is ``known''. i.e. the type of the expression can be
909+determined \emph{without} type checking the \texttt{case}-expression itself.
910+\end{itemize}
911+