ce10256 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tutorial typos

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

2 files changed+3−4

unifiedsplit

tutorial/typesfuns.tex+2−2

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

777777

778778\noindent

779779Again, 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 )}

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

782782\texttt{Vect} of a particular length.

783783

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

847847\begin{SaveVerbatim}{vfiltercons}

848848

849849filter 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' )

851851

852852\end{SaveVerbatim}

853853\useverb{vfiltercons}

tutorial/views.tex+1−2

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

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

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

3939filter 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' )

4241

4342\end{SaveVerbatim}

4443\useverb{vfilterdef}