Gleichheit in Definitionen (entscheidbar Gleichheit? Z Elemente in der Liste ersetzen)

Question

Ich versuche lean zu lernen und eine Ersetzungsfunktion definieren mag, die zwei Elemente nehmen x und y und ersetzt jedes Vorkommen von x mit y in einer vorgegebenen Liste.

Ich habe versucht, es so zu definieren:

def replace {α : Type}: α -> α -> list α -> list α 
| a b [] := [] 
| a b (x::xs) := (if a = x then b else x) :: replace a b xs 

Das gibt mir die folgende Fehlermeldung:

error: failed to synthesize type class instance for 
α : Type, 
replace : α → α → list α → list α, 
a b x : α, 
xs : list α 
⊢ decidable (a = x) 

Mein Problem ist, dass ich nicht Gleichheit für Typen α verwenden kann, so dass ich denke, Ich muss α auf eine Art von Klasse beschränken, wo Gleichheit entscheidbar ist (wie ich in Haskell). Wie kann ich das machen?

Mein aktueller Abhilfe ist die Gleichheit Funktion als Parameter zu übernehmen:

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 

Answer 1

Sie können die entscheidbar Gleichheit von α als eine Art Klassenargument nehmen, wie folgt aus:

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] 

Die eckigen Klammern geben an, dass eine Instanz der Typklasse von der Typklassenauflösung abgeleitet werden sollte.