git.iko.soy/Idris-dev
on master help sign in
Update version number in tutorial
437526aEdwin Brady
tutorial/idris-tutorial.tex+1
compare with master
unifiedsplit
@@ -11,6 +11,7 @@
11\input{library.ltx}
11\input{library.ltx}
12
12
13\newcommand{\Idris}{\textsc{Idris}}
13\newcommand{\Idris}{\textsc{Idris}}
14+\newcommand{\version}{0.9.8}
14
15
15\title{Programming in \Idris{}: a tutorial}
16\title{Programming in \Idris{}: a tutorial}
16\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}
17\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
339an integer, giving 0 if the input is invalid. An example run of this program
339an integer, giving 0 if the input is invalid. An example run of this program
340at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
340at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
341
341
342−\begin{SaveVerbatim}{factrun}
342+\begin{SaveVerbatim}[commandchars=^\{\}]{factrun}
343
343
344$ idris interp.idr
344$ idris interp.idr
345 ____ __ _
345 ____ __ _
346 / _/___/ /____(_)____
346 / _/___/ /____(_)____
347− / // __ / ___/ / ___/ Version 0.9.7
347+ / // __ / ___/ / ___/ Version ^version{}
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.7. The files are available in the \Idris{} distribution,
65+\version{}. 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+6−6
@@ -74,12 +74,12 @@ interactive environment.
74Entering \texttt{idris} at the shell prompt starts up the interactive
74Entering \texttt{idris} at the shell prompt starts up the interactive
75environment. You should see something like the following:
75environment. You should see something like the following:
76
76
77−\begin{SaveVerbatim}{prompt1}
77+\begin{SaveVerbatim}[commandchars=^\{\}]{prompt1}
78
78
79$ idris
79$ idris
80 ____ __ _
80 ____ __ _
81 / _/___/ /____(_)____
81 / _/___/ /____(_)____
82− / // __ / ___/ / ___/ Version 0.9.7
82+ / // __ / ___/ / ___/ Version ^version{}
83 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
83 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
84 /___/\__,_/_/ /_/____/ Type :? for help
84 /___/\__,_/_/ /_/____/ Type :? for help
85
85
@@ -98,8 +98,8 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
98\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
98\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then
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}[commandchars=\\\{\}]{cmds}
102−Idris version 0.9.7
102+Idris version \version{}
103-------------------
103-------------------
104
104
105 Command Arguments Purpose
105 Command Arguments Purpose
@@ -129,12 +129,12 @@ Idris version 0.9.7
129\codefigs{cmds}{Interactive environment commands}
129\codefigs{cmds}{Interactive environment commands}
130
130
131
131
132−\begin{SaveVerbatim}{run1}
132+\begin{SaveVerbatim}[commandchars=^\{\}]{run1}
133
133
134$ idris hello.idr
134$ idris hello.idr
135 ____ __ _
135 ____ __ _
136 / _/___/ /____(_)____
136 / _/___/ /____(_)____
137− / // __ / ___/ / ___/ Version 0.9.7
137+ / // __ / ___/ / ___/ Version ^version{}
138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
139 /___/\__,_/_/ /_/____/ Type :? for help
139 /___/\__,_/_/ /_/____/ Type :? for help
140
140