git.iko.soy/Idris-dev
on master help sign in
Fixed VNil in tutorial (well spotted Cezar :))
856f142Edwin Brady
tutorial/classes.tex+3−3
compare with master
unifiedsplit
@@ -63,9 +63,9 @@ to a \texttt{String}:
63instance Show a => Show (Vect a n) where
63instance Show a => Show (Vect a n) where
64 show xs = "[" ++ show' xs ++ "]" where
64 show xs = "[" ++ show' xs ++ "]" where
65 show' : Show a => Vect a n -> String
65 show' : Show a => Vect a n -> String
66− show' VNil = ""
66+ show' Nil = ""
67− show' (x :: VNil) = show x
67+ show' (x :: Nil) = show x
68− show' (x :: xs) = show x ++ ", " ++ show' xs
68+ show' (x :: xs) = show x ++ ", " ++ show' xs
69
69
70\end{SaveVerbatim}
70\end{SaveVerbatim}
71\useverb{showvec}
71\useverb{showvec}
tutorial/typesfuns.tex+3−3
@@ -388,7 +388,7 @@ Implicit arguments can still be given explicitly in applications, using
388
388
389\begin{SaveVerbatim}{vlookupexp}
389\begin{SaveVerbatim}{vlookupexp}
390
390
391−lookup {a=Int} {n=2} fO (2 :: 3 :: VNil)
391+lookup {a=Int} {n=2} fO (2 :: 3 :: Nil)
392
392
393\end{SaveVerbatim}
393\end{SaveVerbatim}
394\useverb{vlookupexp}
394\useverb{vlookupexp}
@@ -435,7 +435,7 @@ or \texttt{there}, in the tail of the vector. For example:
435\begin{SaveVerbatim}{testelem}
435\begin{SaveVerbatim}{testelem}
436
436
437testVec : Vect Int 4
437testVec : Vect Int 4
438−testVec = 3 :: 4 :: 5 :: 6 :: VNil
438+testVec = 3 :: 4 :: 5 :: 6 :: Nil
439
439
440inVect : Elem 5 testVec
440inVect : Elem 5 testVec
441inVect = there (there here)
441inVect = there (there here)
@@ -833,7 +833,7 @@ If the \texttt{Vect} is empty, the result is easy:
833
833
834\begin{SaveVerbatim}{vfilternil}
834\begin{SaveVerbatim}{vfilternil}
835
835
836−vfilter p VNil = (_ , [])
836+vfilter p Nil = (_ , [])
837
837
838\end{SaveVerbatim}
838\end{SaveVerbatim}
839\useverb{vfilternil}
839\useverb{vfilternil}