@@ -30,6 +30,7 @@ quux = False
3030\end{SaveVerbatim}
3131\useverb{constprims}
3232
33+\noindent
3334An \Idris{} file consists of an optional module declaration (here
3435\texttt{module prims}) followed by an optional list of imports (none here,
3536however \Idris{} programs can consist of several modules, and the definitions
@@ -56,6 +57,7 @@ True : Bool
5657\end{SaveVerbatim}
5758\useverb{promptprim}
5859
60+\noindent
5961All of the usual arithmetic and comparison operators are defined for the primitive
6062types. They are overloaded using type classes, as we will discuss in Section
6163\ref{sec:classes} and can be extended to work on user defined types.
@@ -85,6 +87,7 @@ data List a = Nil | (::) a (List a) -- Polymorphic lists
8587\end{SaveVerbatim}
8688\useverb{natlist}
8789
90+\noindent
8891The above declarations are taken from the standard library. Unary natural
8992numbers can be either zero (\texttt{O} - that's a capital letter 'o', not the digit), or
9093the successor of another natural number (\texttt{S k}).
@@ -100,6 +103,7 @@ infixr 7 ::
100103\end{SaveVerbatim}
101104\useverb{infixcons}
102105
106+\noindent
103107Functions, data constructors and type constuctors may all be given infix
104108operators as names. They may be used in prefix form if enclosed in brackets,
105109e.g. (::). Infix operators can use any of the symbols:
@@ -138,6 +142,7 @@ mult (S k) y = plus y (mult k y)
138142\end{SaveVerbatim}
139143\useverb{natfns}
140144
145+\noindent
141146The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded
142147for use by \texttt{Nat}, and are implemented
143148using the above functions. Unlike Haskell, there is no restriction on whether
@@ -158,6 +163,7 @@ S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
158163\end{SaveVerbatim}
159164\useverb{fntest}
160165
166+\noindent
161167Like arithmetic operations, integer literals are also overloaded using type classes,
162168meaning that we can also test the functions as follows:
163169
@@ -171,6 +177,7 @@ S (S (S (S (S (S (S (S (S (S (S (S O))))))))))) : Nat
171177\end{SaveVerbatim}
172178\useverb{fntest}
173179
180+\noindent
174181You may wonder, by the way, why we have unary natural numbers when our
175182computers have perfectly good integer arithmetic built in. The reason is
176183primarily that unary numbers have a very convenient structure which is easy to
@@ -235,6 +242,7 @@ data Vect : Set -> Nat -> Set where
235242\end{SaveVerbatim}
236243\useverb{vect}
237244
245+\noindent
238246Note that we have used the same constructor names as for \tTC{List}. Ad-hoc
239247name overloading such as this is accepted by \Idris{}, provided that the names
240248are declared in different namespaces (in practice, normally in different modules).
@@ -266,6 +274,7 @@ app (x :: xs) ys = x :: app xs ys
266274\end{SaveVerbatim}
267275\useverb{vapp}
268276
277+\noindent
269278The type of \tFN{app} states that the resulting vector's length will be the sum of
270279the input lengths. If we get the definition wrong in such a way that this does
271280not hold, \Idris{} will not accept the definition. For example:
@@ -290,6 +299,7 @@ $
290299\end{SaveVerbatim}
291300\useverb{vapperrmsg}
292301
302+\noindent
293303This error message suggests that there is a length mismatch between two vectors
294304--- we needed a vector of length \texttt{(S (k + m))}, but provided a vector
295305of length \texttt{(S (k + k))}.
@@ -310,6 +320,7 @@ data Fin : Nat -> Set where
310320\end{SaveVerbatim}
311321\useverb{findecl}
312322
323+\noindent
313324\tDC{fO} is the zeroth element of a finite set with \texttt{S k} elements;
314325\texttt{fS n} is the
315326\texttt{n+1}th element of a finite set with \texttt{S k} elements.
@@ -330,6 +341,7 @@ lookup (fS k) (x :: xs) = lookup k xs
330341\end{SaveVerbatim}
331342\useverb{vlookup}
332343
344+\noindent
333345This function looks up a value at a given location in a vector. The location is
334346bounded by the length of the vector (\texttt{n} in each case), so there is no
335347need for a run-time bounds check. The type checker guarantees that the location
@@ -365,6 +377,7 @@ lookup : {a:Set} -> {n:Nat} -> Fin n -> Vect a n -> a
365377\end{SaveVerbatim}
366378\useverb{vlookupimpty}
367379
380+\noindent
368381Implicit arguments, given in braces \texttt{\{\}} in the type declaration, are not given in
369382applications of \texttt{lookup}; their values can be inferred from the types of
370383the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name which appears as a parameter
@@ -461,6 +474,7 @@ data IO a -- IO operation returning a value of type a
461474\end{SaveVerbatim}
462475\useverb{ioty}
463476
477+\noindent
464478We'll leave the definition of \texttt{IO} abstract, but effectively it describes what
465479the I/O operations to be executed are, rather than how to execute them. The
466480resulting operations are executed externally,
@@ -475,6 +489,7 @@ main = putStrLn "Hello world"
475489\end{SaveVerbatim}
476490\useverb{main}
477491
492+\noindent
478493The type of \texttt{putStrLn} explains that it takes a string, and returns an
479494element of the unit type () via an I/O action. There is a variant \texttt{putStr} which
480495outputs a string without a newline:
@@ -536,6 +551,7 @@ greet = do { putStr "What is your name? "
536551\end{SaveVerbatim}
537552\useverb{greet}
538553
554+\noindent
539555The syntax \texttt{x <- iovalue} executes the I/O operation iovalue, of type
540556\texttt{IO a}, and
541557puts the result, of type \texttt{a} into the variabel \texttt{x}.
@@ -694,7 +710,7 @@ bounds error:
694710\begin{SaveVerbatim}{lookuplist}
695711
696712list_lookup : Nat -> List a -> Maybe a
697−list_lookup _ Nil = Nothing
713+list_lookup _ Nil = Nothing
698714list_lookup O (x :: xs) = Just x
699715list_lookup (S k) (x :: xs) = list_lookup k xs
700716