ce10256 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Tutorial typos

ce10256Edwin Brady15 years ago

tutorial/typesfuns.tex+2−2

@@ -777,7 +777,7 @@ data Exists : (A : Set) -> (P : A -> Set) -> Set where

777

778\noindent

779Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of

780−A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p (}

780+A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p )}

781constructs a value of this type. For example, we can pair a number with a

782\texttt{Vect} of a particular length.

783

@@ -847,7 +847,7 @@ notation. with allows pattern matching on intermediate values:

847\begin{SaveVerbatim}{vfiltercons}

848

849filter p (x :: xs) with (filter p xs)

850− | (_ , xs') = if (p x) then (_ , x :: xs') else (_ , xs')

850+ | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

851

852\end{SaveVerbatim}

853\useverb{vfiltercons}

tutorial/views.tex+1−2

@@ -37,8 +37,7 @@ a vector filter function, defined as follows:

37filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)

38filter p [] = ( _ ** [] )

39filter p (x :: xs) with (filter p xs)

40− | ( _ ** xs' )

41− = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

40+ | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

43\end{SaveVerbatim}

42\end{SaveVerbatim}

44\useverb{vfilterdef}

43\useverb{vfilterdef}