git.iko.soy/Idris-dev
on master help sign in
Error message in tutorial
4b63e6eEdwin Brady
tutorial/examples/prims.idrnew file+14
compare with master
unifiedsplit
@@ -0,0 +1,14 @@
1+module prims;
2+
3+x : Int;
4+x = 42;
5+
6+foo : String;
7+foo = "Sausage machine";
8+
9+bar : Char;
10+bar = 'Z';
11+
12+quux : Bool;
13+quux = False;
14+
tutorial/examples/vbroken.idrnew file+6
@@ -0,0 +1,6 @@
1+
2+vapp : Vect a n -> Vect a m -> Vect a (n + m);
3+vapp Nil ys = ys;
4+vapp (x :: xs) ys = x :: vapp xs xs; -- BROKEN
5+
6+
tutorial/typesfuns.tex+5−3
@@ -235,14 +235,16 @@ app (x :: xs) ys = x :: app xs xs; -- BROKEN
235
235
236\begin{SaveVerbatim}{vapperrmsg}
236\begin{SaveVerbatim}{vapperrmsg}
237
237
238−$ idris app.idr --check
238+$ idris vbroken.idr --check
239−app.idr:3:Can't unify Vect a m with Vect a (plus n m)
239+vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m))
240
240
241\end{SaveVerbatim}
241\end{SaveVerbatim}
242\useverb{vapperrmsg}
242\useverb{vapperrmsg}
243%$
243%$
244
244
245−This error message suggests that there is a length mismatch between two vectors.
245+This error message suggests that there is a length mismatch between two vectors
246+--- we needed a vector of length \texttt{(S (k + m))}, but provided a vector
247+of length \texttt{(S (k + k))}.
246Note that the terms in the error message have been \emph{normalised}, so in
248Note that the terms in the error message have been \emph{normalised}, so in
247particular \texttt{n + m} has been reduced to \texttt{plus n m}.
249particular \texttt{n + m} has been reduced to \texttt{plus n m}.
248
250