git.iko.soy/Idris-dev
on master help sign in
Tutorial typos fixed
commitae1cf5338d4f726c448b5671de658a6e054232c1 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 3 Feb 2012, 11:50 (15 years ago) parent5399670
6 files changed+11−14
compare with master
unifiedsplit
CHANGELOG+4−5 tutorial/idris-tutorial.pdf tutorial/provisional.tex+2−4 tutorial/starting.tex+1−1 tutorial/theorems.tex+1−1 tutorial/typesfuns.tex+3−3
CHANGELOG+4−5
@@ -3,14 +3,13 @@ New in 0.9.1:
33
44User visible changes:
55
6−* DSL notation
7−* Record projection and update
6+* DSL notation, for overloading lambda and let bindings
7+* Dependent records, with projection and update
88* Totality checking and 'total' keyword
99* Auto implicits and default argument values {auto n : T}, {default val n : T}
10−* Additions to prelude, including Nat and List theorems
1110* Overlapping type class instances disallowed
12−* Many extensions to nat and list libraries (mostly thanks to Dominic
13− Mulligan)
11+* Many extensions to prelude.nat and prelude.list libraries (mostly thanks to
12+ Dominic Mulligan)
1413* New libraries: control.monad.identity, control.monad.state
1514* Small improvements in error reporting
1615
tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/provisional.tex+2−4
@@ -24,10 +24,9 @@ We'd like to implement this as follows:
2424parity : (n:Nat) -> Parity n
2525parity O = even {n=O}
2626parity (S O) = odd {n=O}
27−parity (S (S k)) with parity k {
27+parity (S (S k)) with (parity k)
2828 parity (S (S (j + j))) | even = even {n=S j}
2929 parity (S (S (S (j + j)))) | odd = odd {n=S j}
30−}
3130
3231\end{SaveVerbatim}
3332\useverb{parfail}
@@ -80,10 +79,9 @@ except that they introduce the right hand side with a \texttt{?=} rathar than
8079parity : (n:Nat) -> Parity n
8180parity O = even {n=O}
8281parity (S O) = odd {n=O}
83−parity (S (S k)) with parity k {
82+parity (S (S k)) with (parity k)
8483 parity (S (S (j + j))) | even ?= even {n=S j}
8584 parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
86−}
8785
8886\end{SaveVerbatim}
8987\useverb{paritypro}
tutorial/starting.tex+1−1
@@ -22,7 +22,7 @@ The easiest way to install \Idris{}, if you have all of the prerequisites, is to
2222
2323\begin{SaveVerbatim}{install}
2424
25−cabal install idris
25+cabal update; cabal install idris
2626
2727\end{SaveVerbatim}
2828\useverb{install}
tutorial/theorems.tex+1−1
@@ -345,7 +345,7 @@ from which we could prove anything:
345345
346346\begin{SaveVerbatim}{empties}
347347
348−-- making use of 'head' being partially defined
348+-- making use of 'hd' being partially defined
349349empty1 : _|_
350350empty1 = hd [] where
351351 hd : List a -> a
tutorial/typesfuns.tex+3−3
@@ -557,7 +557,7 @@ greet = do putStr "What is your name? "
557557\useverb{greet}
558558
559559\noindent
560−The syntax \texttt{x <- iovalue} executes the I/O operation iovalue, of type
560+The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type
561561\texttt{IO a}, and
562562puts the result, of type \texttt{a} into the variable \texttt{x}.
563563In this case, \texttt{getLine} returns an \texttt{IO String},
@@ -608,7 +608,7 @@ names \texttt{Nil} and \texttt{::} can be written in list form. For example:
608608
609609\begin{itemize}
610610\item \texttt{[]} means \texttt{Nil}
611−\item \texttt{[1,2,3]} means \texttt{Cons 1 (Cons 2 (Cons 3 Nil))}
611+\item \texttt{[1,2,3]} means \texttt{1 :: 2 :: 3 :: Nil}
612612\end{itemize}
613613
614614\noindent
@@ -849,7 +849,7 @@ filter p Nil = (_ , [])
849849In the \texttt{::} case, we need to inspect the result of a recursive call to
850850\texttt{filter} to
851851extract the length and the vector from the result. To do this, we use \texttt{with}
852−notation. with allows pattern matching on intermediate values:
852+notation, which allows pattern matching on intermediate values:
853853
854854\begin{SaveVerbatim}{vfiltercons}
855855