reverse_vect.idr

module reverse_vect

import Data.Vect

myReverse : Vect n a -> Vect n a
myReverse [] = []
myReverse (x::xs) = (myReverse xs) ++ [x]

Hi, it should be:

module reverse_vect

import Data.Vect

myReverse : Vect n a -> Vect n a
myReverse [] = []
myReverse {n = S k} (x::xs) = rewrite plusCommutative 1 k in (myReverse xs) ++ [x]

The reason that k + 1 is not S k is that + is defined to recurse on the left argument in Nat. So k + 1 would not reduce any further since k is unknown rewriting with plusCommutative ensures that the arguments are flipped so that k + 1 becomes 1 + k which can reduce to S k. The reason that the type of myReverse xs ++ [x] is k + 1 is because of the definition of ++ which adds the length of the given arguments in the resulting Vect 😄