I am trying to learn lean and want to define a replace function, which takes two elements x and y and replaces every occurrence of x with y in a given list.
I tried to define it like this:
def replace {α : Type}: α -> α -> list α -> list α
| a b [] := []
| a b (x::xs) := (if a = x then b else x) :: replace a b xs
This gives me the following error:
error: failed to synthesize type class instance for
α : Type,
replace : α → α → list α → list α,
a b x : α,
xs : list α
⊢ decidable (a = x)
My problem is that I cannot use equality for type α, so I guess I need to restrict α to be of some kind of type class where equality is decidable (like I would in Haskell). How can I do this?
My current workaround is to take the equality function as a parameter:
def replace {α : Type}: (α -> α -> bool) -> α -> α -> list α -> list α
| eq a b [] := []
| eq a b (x::xs) := (if eq a x then b else x) :: replace eq a b xs
You can take the decidable equality of α as a type class argument, like this:
def replace {α : Type} [decidable_eq α] : α -> α -> list α -> list α
| a b [] := []
| a b (x::xs) := (if a = x then b else x) :: replace a b xs
#eval replace 2 3 [2, 2, 5, 6, 3, 2]
The square brackets denote that an instance of the type class should be inferred by type class resolution.