title: Equality in definitions (decidable equality? e.g. replace elements in list)
body: <p>I am trying to learn <a href="https://leanprover.github.io/" rel="nofollow noreferrer">lean</a> and want to define a replace function, which takes two elements <code>x</code> and <code>y</code> and replaces every occurrence of <code>x</code> with <code>y</code> in a given list.</p>
  
  <p>I tried to define it like this:</p>
  
  <pre><code>def replace {α : Type}: α -&gt; α -&gt; list α -&gt; list α
  | a b [] := []
  | a b (x::xs) := (if a = x then b else x) :: replace a b xs
  </code></pre>
  
  <p>This gives me the following error:</p>
  
  <pre><code>error: failed to synthesize type class instance for
  α : Type,
  replace : α → α → list α → list α,
  a b x : α,
  xs : list α
  ⊢ decidable (a = x)
  </code></pre>
  
  <p>My problem is that I <strong>cannot use equality for type <code>α</code></strong>, so I guess I need to restrict <code>α</code> to be of some kind of type class where equality is decidable (like I would in Haskell). How can I do this?</p>
  
  <p>My current <strong>workaround</strong> is to take the equality function as a parameter:</p>
  
  <pre><code>def replace {α : Type}: (α -&gt; α -&gt; bool) -&gt; α -&gt; α -&gt; list α -&gt; list α
  | eq a b [] := []
  | eq a b (x::xs) := (if eq a x then b else x) :: replace eq a b xs
  </code></pre>