@@ -382,7 +382,7 @@ definition:
382382
383383 vadd : Vect n Int -> Vect n Int -> Vect n Int
384384 vadd [] [] = []
385− vadd (x :: idris xs) (y :: ys) = x + y :: vadd xs ys
385+ vadd (x :: xs) (y :: ys) = x + y :: vadd xs ys
386386
387387Using , we can set up a program so that it reads input from a user,
388388checks that the input is valid (i.e both vectors contain integers, and
@@ -410,10 +410,28 @@ following type:
410410
411411This returns a dependent pair of a length, and a vector of that
412412length, because we cannot know in advance how many integers the user
413−is going to input. One way to implement this function, using ``-1`` to
414−indicate the end of input, is shown in Listing [readvec]. This uses a
415−variation on ``parseNumber`` which does not require a number to be
416−within range.
413+is going to input. We can use ``-1`` to indicate the end of input:
414+
415+.. code-block:: idris
416+
417+ read_vec : Eff (p ** Vect p Int) [STDIO]
418+ read_vec = do putStr "Number (-1 when done): "
419+ case the (Maybe Int) $ run (parseNumber (trim !getStr)) of
420+ Nothing => do putStrLn "Input error"
421+ read_vec
422+ Just v => if (v /= -1)
423+ then do (_ ** xs) <- read_vec
424+ pure (_ ** v :: xs)
425+ else pure (_ ** [])
426+ where
427+ parseNumber : String -> Eff Int [EXCEPTION String]
428+ parseNumber str
429+ = if all (\x => isDigit x || x == '-') (unpack str)
430+ then pure (cast str)
431+ else raise "Not a number"
432+
433+This uses a variation on ``parseNumber`` which does not require a
434+number to be within range.
417435
418436Finally, we write a program which reads two vectors and prints the
419437result of pairwise addition of them, throwing an exception if the
@@ -434,23 +452,6 @@ equal. This does not stop us reading vectors from user input, but it
434452does require that the lengths are checked and any discrepancy is dealt
435453with gracefully.
436454
437−.. code-block:: idris
438−
439− read_vec : Eff (p ** Vect p Int) [STDIO]
440− read_vec = do putStr "Number (-1 when done): "
441− case run (parseNumber (trim !getStr)) of
442− Nothing => do putStrLn "Input error"
443− read_vec
444− Just v => if (v /= -1)
445− then do (_ ** xs) <- read_vec
446− pure (_ ** v :: xs)
447− else pure (_ ** [])
448− where
449− parseNumber : String -> Eff Int [EXCEPTION String]
450− parseNumber str
451− = if all (\x => isDigit x || x == '-') (unpack str)
452− then pure (cast str)
453− else raise "Not a number"
454455
455456Example: An Expression Calculator
456457=================================