git.iko.soy/Idris-dev
on master help sign in
Minor tutorial updates
69d3216Edwin Brady
tutorial/interp.tex+1−1
compare with master
unifiedsplit
@@ -344,7 +344,7 @@ at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
344$ idris interp.idr
344$ idris interp.idr
345 ____ __ _
345 ____ __ _
346 / _/___/ /____(_)____
346 / _/___/ /____(_)____
347− / // __ / ___/ / ___/ Version 0.9.6
347+ / // __ / ___/ / ___/ Version 0.9.7
348 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
348 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
349 /___/\__,_/_/ /_/____/ Type :? for help
349 /___/\__,_/_/ /_/____/ Type :? for help
350
350
tutorial/intro.tex+1−1
@@ -62,7 +62,7 @@ verifying systems software.
62\subsection{Example Code}
62\subsection{Example Code}
63
63
64This tutorial includes some example code, which has been tested with \Idris{} version
64This tutorial includes some example code, which has been tested with \Idris{} version
65−0.9.6. The files are available in the \Idris{} distribution,
65+0.9.7. The files are available in the \Idris{} distribution,
66so that you can try them out easily,
66so that you can try them out easily,
67under \texttt{tutorial/examples}. However, it is strongly recommended that you
67under \texttt{tutorial/examples}. However, it is strongly recommended that you
68type them in yourself, rather than simply loading and reading them.
68type them in yourself, rather than simply loading and reading them.
tutorial/starting.tex+3−3
@@ -79,7 +79,7 @@ environment. You should see something like the following:
79$ idris
79$ idris
80 ____ __ _
80 ____ __ _
81 / _/___/ /____(_)____
81 / _/___/ /____(_)____
82− / // __ / ___/ / ___/ Version 0.9.6
82+ / // __ / ___/ / ___/ Version 0.9.7
83 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
83 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
84 /___/\__,_/_/ /_/____/ Type :? for help
84 /___/\__,_/_/ /_/____/ Type :? for help
85
85
@@ -99,7 +99,7 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
99the program is compiled to the executable \texttt{hello}.
99the program is compiled to the executable \texttt{hello}.
100
100
101\begin{SaveVerbatim}{cmds}
101\begin{SaveVerbatim}{cmds}
102−Idris version 0.9.6
102+Idris version 0.9.7
103-------------------
103-------------------
104
104
105 Command Arguments Purpose
105 Command Arguments Purpose
@@ -134,7 +134,7 @@ Idris version 0.9.6
134$ idris hello.idr
134$ idris hello.idr
135 ____ __ _
135 ____ __ _
136 / _/___/ /____(_)____
136 / _/___/ /____(_)____
137− / // __ / ___/ / ___/ Version 0.9.6
137+ / // __ / ___/ / ___/ Version 0.9.7
138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
139 /___/\__,_/_/ /_/____/ Type :? for help
139 /___/\__,_/_/ /_/____/ Type :? for help
140
140
tutorial/typesfuns.tex+6−6
@@ -333,10 +333,10 @@ not hold, \Idris{} will not accept the definition. For example:
333\begin{SaveVerbatim}{vapperrmsg}
333\begin{SaveVerbatim}{vapperrmsg}
334
334
335$ idris vbroken.idr --check
335$ idris vbroken.idr --check
336−vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m))
336+vbroken.idr:3:Can't unify Vect a n with Vect a m
337
337
338Specifically:
338Specifically:
339− Can't unify k with m
339+ Can't unify n with m
340
340
341\end{SaveVerbatim}
341\end{SaveVerbatim}
342\begin{SaveVerbatim}{bleh}
342\begin{SaveVerbatim}{bleh}
@@ -346,10 +346,10 @@ $
346
346
347\noindent
347\noindent
348This error message suggests that there is a length mismatch between two vectors
348This error message suggests that there is a length mismatch between two vectors
349−--- we needed a vector of length \texttt{(S (k + m))}, but provided a vector
349+--- we needed a vector of length \texttt{m}, but provided a vector
350−of length \texttt{(S (k + k))}.
350+of length \texttt{n}.
351−Note that the terms in the error message have been \emph{normalised}, so in
351+%Note that the terms in the error message have been \emph{normalised}, so in
352−particular \texttt{n + m} has been reduced to \texttt{plus n m}.
352+%particular \texttt{n + m} has been reduced to \texttt{plus n m}.
353
353
354\subsubsection{The Finite Sets}
354\subsubsection{The Finite Sets}
355
355