Hugues Chabot (2) [Avatar] Offline
#1
Step 6 states that "This case does type check, so we can't use impossible."

However, with Idris 0.11.2, if I use "Proof search" I get the following implementation. If this is the new Idris behaviour, the instructions should reflect that.

removeElem : (value : a) -> (xs : Vect (S n) a) -> Elem value xs -> Vect n a
removeElem value (value :: ys) Here = ys
removeElem {n = Z} _ (_ :: []) (There Here) impossible
removeElem {n = Z} _ (_ :: []) (There (There _)) impossible
removeElem {n = (S k)} value (y :: ys) (There later) = y :: (removeElem value ys later)
Hugues Chabot (2) [Avatar] Offline
#2
My bad. I used my own implementation of Vect to avoid conflict with Elem. If I provide the following implementation, I can use absurd in removeElem.

Uninhabited (Elem value []) where
    uninhabited Here impossible
    uninhabited (There _) impossible