holesWithRewrites.idr

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse {n = S k} (x :: xs) 
          = let result = myReverse xs ++ [x] in
                rewrite plusCommutative 1 k in ?myReverse_rhs_2

{- my holes
 elem : Type
 k : Nat
 x : elem
 xs : Vect k elem
 result : Vect (k + 1) elem
 _rewrite_rule : fromInteger 1 + k = k + fromInteger 1
-----------------------------------------------------------------------------------
myReverse_rhs_2 : (\replaced => Vect replaced elem) (plus k (fromInteger 1))
-}

{- copied from textbook page 224
  elem : Type
  k : Nat
  x : elem
  xs : Vect k elem
  result : Vect (plus k 1) elem
  _rewrite_rule : plus k 1 = S k
--------------------------------------
myReverse_rhs_2 : Vect (plus k 1) elem
-}

I'm using Idris Version 1.1.1

I'm also using Emacs idris-mode 20171212.759