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

tutorial/interp.tex+2−2

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

330

331\noindent

332Here, \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

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

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

336

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

367

368\noindent

369It 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}

371parameters at the point where the cast is applied.

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

373they make sense.

tutorial/modules.tex+1−1

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

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

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

87is 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.

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

90\end{itemize}

91

tutorial/typesfuns.tex+1−1

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

938

939\noindent

940\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

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

943

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