git.iko.soy/Idris-dev
on master help sign in
Update version number in tutorial
commit437526aa4d85ef4d73eaf7118a01af1b776af64e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 14 Apr 2013, 15:21 (14 years ago) parent809683b
4 files changed+10−9
compare with master
unifiedsplit
tutorial/idris-tutorial.tex+1 tutorial/interp.tex+2−2 tutorial/intro.tex+1−1 tutorial/starting.tex+6−6
tutorial/idris-tutorial.tex+1
@@ -11,6 +11,7 @@
1111\input{library.ltx}
1212
1313\newcommand{\Idris}{\textsc{Idris}}
14+\newcommand{\version}{0.9.8}
1415
1516\title{Programming in \Idris{}: a tutorial}
1617\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}
tutorial/interp.tex+2−2
@@ -339,12 +339,12 @@ type to another if possible. Here, it converts a string to
339339an integer, giving 0 if the input is invalid. An example run of this program
340340at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
341341
342−\begin{SaveVerbatim}{factrun}
342+\begin{SaveVerbatim}[commandchars=^\{\}]{factrun}
343343
344344$ idris interp.idr
345345 ____ __ _
346346 / _/___/ /____(_)____
347− / // __ / ___/ / ___/ Version 0.9.7
347+ / // __ / ___/ / ___/ Version ^version{}
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.7. The files are available in the \Idris{} distribution,
65+\version{}. 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+6−6
@@ -74,12 +74,12 @@ interactive environment.
7474Entering \texttt{idris} at the shell prompt starts up the interactive
7575environment. You should see something like the following:
7676
77−\begin{SaveVerbatim}{prompt1}
77+\begin{SaveVerbatim}[commandchars=^\{\}]{prompt1}
7878
7979$ idris
8080 ____ __ _
8181 / _/___/ /____(_)____
82− / // __ / ___/ / ___/ Version 0.9.7
82+ / // __ / ___/ / ___/ Version ^version{}
8383 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
8484 /___/\__,_/_/ /_/____/ Type :? for help
8585
@@ -98,8 +98,8 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
9898\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
9999the program is compiled to the executable \texttt{hello}.
100100
101−\begin{SaveVerbatim}{cmds}
102−Idris version 0.9.7
101+\begin{SaveVerbatim}[commandchars=\\\{\}]{cmds}
102+Idris version \version{}
103103-------------------
104104
105105 Command Arguments Purpose
@@ -129,12 +129,12 @@ Idris version 0.9.7
129129\codefigs{cmds}{Interactive environment commands}
130130
131131
132−\begin{SaveVerbatim}{run1}
132+\begin{SaveVerbatim}[commandchars=^\{\}]{run1}
133133
134134$ idris hello.idr
135135 ____ __ _
136136 / _/___/ /____(_)____
137− / // __ / ___/ / ___/ Version 0.9.7
137+ / // __ / ___/ / ___/ Version ^version{}
138138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
139139 /___/\__,_/_/ /_/____/ Type :? for help
140140