The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

371392 (9) [Avatar] Offline
#1
(MEAP v12, Idris 0.12.3)

In exercise 8.2.6.2, if I type in the skeleton definition in the book:

my_reverse : Vect n a -> Vect n a
my_reverse xs = reverse' [] xs
  where
    reverse' : Vect n a -> Vect m a -> Vect (n+m) a
    reverse' acc []        = ?revPrfNil acc
    reverse' acc (x :: xs) = ?revPrfXs (reverse' (x :: acc) xs)


… I don't get the nice listing of holes, but instead the following error:


     When checking left hand side of Main.my_reverse, reverse':
     Type mismatch between
             Vect {a = Type} (S k) a (Type of x :: xs)
     and
             Vect {a = ty} (S k) a (Expected type)
     
     Specifically:
             Type mismatch between
                     Type
             and
                     ty


After some fumbling around, I found a way to make the error go away, but I don't really know why this works, nor what the original error meant.

my_reverse : {a : Type} -> Vect n a -> Vect n a
my_reverse xs = reverse' [] xs
  where
    reverse' : {a : Type} -> Vect n a -> Vect m a -> Vect (n+m) a
    reverse' acc []        = ?revPrfNil acc
    reverse' acc (x :: xs) = ?revPrfXs (reverse' (x :: acc) xs)


Is this expected behaviour here? Did I do something wrong?
371392 (9) [Avatar] Offline
#2
Turns out that my own Vect definition was wrong… Sorry for the noise. smilie