dependent elimination failed

Stream: new members

[Vivek Rajesh Joshi]

I'm defining a new function to erase all occurences of an element in a list. Why does it not work with a DecidableEq instance?

def list_eraseAll [DecidableEq α] : List α → α → List α
  | [],    _ => []
  | a::as, b => match a = b with
    | true  => list_eraseAll as b
    | false => a :: list_eraseAll as b

error:

dependent elimination failed, type mismatch when solving alternative with type
  motive (true = true)
but expected
  motive x✝

[Damiano Testa]

Try using == instead of = (= is Prop-valued, while == is Bool-valued)

[Vivek Rajesh Joshi]

It works, but what goes wrong with the Prop-valued =?

[Chris Bailey]

It's not an inductive type with two constructors 'false' and 'true'.

[Vivek Rajesh Joshi]

Ahh okay, got it

[Chris Bailey]

You can use the DecidableEq instance in its prop form with an if-then-else:

def list_eraseAll [DecidableEq α] : List α → α → List α
  | [],    _ => []
  | a::as, b =>
    if a = b
    then list_eraseAll as b
    else a :: list_eraseAll as b

[Vivek Rajesh Joshi]

I see, thanks!