5ef6475 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tutorial typos

commit5ef64757b241300fcfa0aed23ed36b15ce6a2d58 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 13 Jan 2012, 15:26 (15 years ago) parentd1d672e

3 files changed+4−4

unifiedsplit

tutorial/interp.tex+2−2

@@ -330,7 +330,7 @@ main = do putStr "Enter a number: "

330330

331331\noindent

332332Here, \texttt{cast} is an overloaded function which converts a value from one

333−type to another if possible. Here, it conversts a string to

333+type to another if possible. Here, it converts a string to

334334an integer, giving 0 if the input is invalid. An example run of this program

335335at the \Idris{} interactive environment is shown in Figure \ref{factrun}.

336336

@@ -367,7 +367,7 @@ class Cast from to where

367367

368368\noindent

369369It is a \emph{multi-parameter} type class, defining the source type and object

370−type of the cast. It must be possible for the type checker \remph{both}

370+type of the cast. It must be possible for the type checker to infer \remph{both}

371371parameters at the point where the cast is applied.

372372There are casts defined between all of the primitive types, as far as

373373they make sense.

tutorial/modules.tex+1−1

@@ -85,7 +85,7 @@ method names are exported.

8585\item \texttt{abstract} means that only the name is exported. For functions, this means

8686that the implementation is not exported. For data types, this means that the type name

8787is exported but not the constructors. For classes, this means that the class name is exported

88−but not the method names/

88+but not the method names.

8989\item \texttt{private} means that neither the name nor the definition is exported.

9090\end{itemize}

9191

tutorial/typesfuns.tex+1−1

@@ -938,7 +938,7 @@ splitAt c x = case break (== c) x of

938938

939939\noindent

940940\texttt{break} is a library function which breaks a string into a pair of strings

941−at the point where the given function is no longer true. We then deconstruct the

941+at the point where the given function returns true. We then deconstruct the

942942pair it returns, and remove the first character of the second string.

943943

944944A \texttt{case} expression can match several cases, for example, to inspect an