Permalink
Browse files

Tutorial typos fixed

  • Loading branch information...
Edwin Brady
Edwin Brady committed Feb 3, 2012
1 parent 5399670 commit ae1cf5338d4f726c448b5671de658a6e054232c1
View
@@ -3,14 +3,13 @@ New in 0.9.1:
User visible changes:
-* DSL notation
-* Record projection and update
+* DSL notation, for overloading lambda and let bindings
+* Dependent records, with projection and update
* Totality checking and 'total' keyword
* Auto implicits and default argument values {auto n : T}, {default val n : T}
-* Additions to prelude, including Nat and List theorems
* Overlapping type class instances disallowed
-* Many extensions to nat and list libraries (mostly thanks to Dominic
- Mulligan)
+* Many extensions to prelude.nat and prelude.list libraries (mostly thanks to
+ Dominic Mulligan)
* New libraries: control.monad.identity, control.monad.state
* Small improvements in error reporting
View
Binary file not shown.
View
@@ -24,10 +24,9 @@ \section{Provisional Definitions}
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
-parity (S (S k)) with parity k {
+parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even = even {n=S j}
parity (S (S (S (j + j)))) | odd = odd {n=S j}
-}
\end{SaveVerbatim}
\useverb{parfail}
@@ -80,10 +79,9 @@ \subsection{Provisional definitions}
parity : (n:Nat) -> Parity n
parity O = even {n=O}
parity (S O) = odd {n=O}
-parity (S (S k)) with parity k {
+parity (S (S k)) with (parity k)
parity (S (S (j + j))) | even ?= even {n=S j}
parity (S (S (S (j + j)))) | odd ?= odd {n=S j}
-}
\end{SaveVerbatim}
\useverb{paritypro}
View
@@ -22,7 +22,7 @@ \subsection{Downloading and Installing}
\begin{SaveVerbatim}{install}
-cabal install idris
+cabal update; cabal install idris
\end{SaveVerbatim}
\useverb{install}
View
@@ -345,7 +345,7 @@ \subsection{Totality Checking}
\begin{SaveVerbatim}{empties}
--- making use of 'head' being partially defined
+-- making use of 'hd' being partially defined
empty1 : _|_
empty1 = hd [] where
hd : List a -> a
View
@@ -557,7 +557,7 @@ \subsection{``\texttt{do}'' notation}
\useverb{greet}
\noindent
-The syntax \texttt{x <- iovalue} executes the I/O operation iovalue, of type
+The syntax \texttt{x <- iovalue} executes the I/O operation \texttt{iovalue}, of type
\texttt{IO a}, and
puts the result, of type \texttt{a} into the variable \texttt{x}.
In this case, \texttt{getLine} returns an \texttt{IO String},
@@ -608,7 +608,7 @@ \subsubsection{\texttt{List} and \texttt{Vect}}
\begin{itemize}
\item \texttt{[]} means \texttt{Nil}
-\item \texttt{[1,2,3]} means \texttt{Cons 1 (Cons 2 (Cons 3 Nil))}
+\item \texttt{[1,2,3]} means \texttt{1 :: 2 :: 3 :: Nil}
\end{itemize}
\noindent
@@ -849,7 +849,7 @@ \subsubsection*{Dependent Pairs}
In the \texttt{::} case, we need to inspect the result of a recursive call to
\texttt{filter} to
extract the length and the vector from the result. To do this, we use \texttt{with}
-notation. with allows pattern matching on intermediate values:
+notation, which allows pattern matching on intermediate values:
\begin{SaveVerbatim}{vfiltercons}

0 comments on commit ae1cf53

Please sign in to comment.