git.iko.soy/Idris-dev
on master help sign in
Minor tutorial updates
commit69d32168231c75d1b91ef27a8f7007d747b86c7a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 10 Mar 2013, 21:34 (14 years ago) parent109f2d7
4 files changed+11−11
compare with master
unifiedsplit
tutorial/interp.tex+1−1 tutorial/intro.tex+1−1 tutorial/starting.tex+3−3 tutorial/typesfuns.tex+6−6
tutorial/interp.tex+1−1
@@ -344,7 +344,7 @@ at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
344344$ idris interp.idr
345345 ____ __ _
346346 / _/___/ /____(_)____
347− / // __ / ___/ / ___/ Version 0.9.6
347+ / // __ / ___/ / ___/ Version 0.9.7
348348 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
349349 /___/\__,_/_/ /_/____/ Type :? for help
350350
tutorial/intro.tex+1−1
@@ -62,7 +62,7 @@ verifying systems software.
6262\subsection{Example Code}
6363
6464This 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,
6666so that you can try them out easily,
6767under \texttt{tutorial/examples}. However, it is strongly recommended that you
6868type 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:
7979$ idris
8080 ____ __ _
8181 / _/___/ /____(_)____
82− / // __ / ___/ / ___/ Version 0.9.6
82+ / // __ / ___/ / ___/ Version 0.9.7
8383 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
8484 /___/\__,_/_/ /_/____/ Type :? for help
8585
@@ -99,7 +99,7 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
9999the program is compiled to the executable \texttt{hello}.
100100
101101\begin{SaveVerbatim}{cmds}
102−Idris version 0.9.6
102+Idris version 0.9.7
103103-------------------
104104
105105 Command Arguments Purpose
@@ -134,7 +134,7 @@ Idris version 0.9.6
134134$ idris hello.idr
135135 ____ __ _
136136 / _/___/ /____(_)____
137− / // __ / ___/ / ___/ Version 0.9.6
137+ / // __ / ___/ / ___/ Version 0.9.7
138138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
139139 /___/\__,_/_/ /_/____/ Type :? for help
140140
tutorial/typesfuns.tex+6−6
@@ -333,10 +333,10 @@ not hold, \Idris{} will not accept the definition. For example:
333333\begin{SaveVerbatim}{vapperrmsg}
334334
335335$ 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
337337
338338Specifically:
339− Can't unify k with m
339+ Can't unify n with m
340340
341341\end{SaveVerbatim}
342342\begin{SaveVerbatim}{bleh}
@@ -346,10 +346,10 @@ $
346346
347347\noindent
348348This 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
350−of length \texttt{(S (k + k))}.
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}.
349+--- we needed a vector of length \texttt{m}, but provided a vector
350+of length \texttt{n}.
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}.
353353
354354\subsubsection{The Finite Sets}
355355