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.

Hugues Chabot (2) [Avatar] Offline
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
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