856f142 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixed VNil in tutorial (well spotted Cezar :))

commit856f142f52bb39fbf94ab254bc62d69d5b5e01f9 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 13 Jan 2012, 12:53 (15 years ago) parent6e699c7

2 files changed+6−6

compare with master

unifiedsplit

tutorial/classes.tex+3−3 tutorial/typesfuns.tex+3−3

tutorial/classes.tex+3−3

@@ -63,9 +63,9 @@ to a \texttt{String}:

6363instance Show a => Show (Vect a n) where

6464 show xs = "[" ++ show' xs ++ "]" where

6565 show' : Show a => Vect a n -> String

66− show' VNil = ""

67− show' (x :: VNil) = show x

68− show' (x :: xs) = show x ++ ", " ++ show' xs

66+ show' Nil = ""

67+ show' (x :: Nil) = show x

68+ show' (x :: xs) = show x ++ ", " ++ show' xs

6969

7070\end{SaveVerbatim}

7171\useverb{showvec}

tutorial/typesfuns.tex+3−3

@@ -388,7 +388,7 @@ Implicit arguments can still be given explicitly in applications, using

388388

389389\begin{SaveVerbatim}{vlookupexp}

390390

391−lookup {a=Int} {n=2} fO (2 :: 3 :: VNil)

391+lookup {a=Int} {n=2} fO (2 :: 3 :: Nil)

392392

393393\end{SaveVerbatim}

394394\useverb{vlookupexp}

@@ -435,7 +435,7 @@ or \texttt{there}, in the tail of the vector. For example:

435435\begin{SaveVerbatim}{testelem}

436436

437437testVec : Vect Int 4

438−testVec = 3 :: 4 :: 5 :: 6 :: VNil

438+testVec = 3 :: 4 :: 5 :: 6 :: Nil

439439

440440inVect : Elem 5 testVec

441441inVect = there (there here)

@@ -833,7 +833,7 @@ If the \texttt{Vect} is empty, the result is easy:

833833

834834\begin{SaveVerbatim}{vfilternil}

835835

836−vfilter p VNil = (_ , [])

836+vfilter p Nil = (_ , [])

837837

838838\end{SaveVerbatim}

839839\useverb{vfilternil}