git.iko.soy/Idris-dev
on master help sign in
Error message in tutorial
commit4b63e6eb915720a29a5a39fe93a9ffce0d0a7df0 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 18 Dec 2011, 16:30 (15 years ago) parent1fa2dfa
3 files changed+25−3
compare with master
unifiedsplit
tutorial/examples/prims.idr+14 tutorial/examples/vbroken.idr+6 tutorial/typesfuns.tex+5−3
tutorial/examples/prims.idrnew file+14
@@ -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
235235
236236\begin{SaveVerbatim}{vapperrmsg}
237237
238−$ idris app.idr --check
239−app.idr:3:Can't unify Vect a m with Vect a (plus n m)
238+$ idris vbroken.idr --check
239+vbroken.idr:3:Can't unify Vect a (S (plus k k)) with Vect a (S (plus k m))
240240
241241\end{SaveVerbatim}
242242\useverb{vapperrmsg}
243243%$
244244
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))}.
246248Note that the terms in the error message have been \emph{normalised}, so in
247249particular \texttt{n + m} has been reduced to \texttt{plus n m}.
248250