## Stream: new members

### Topic: Getting unification info from lean

#### Chris B (Jul 31 2019 at 23:15):

If I try to define nat.succ_add as it is in core for some arbitrary type with the same shape as nat (or using anything with the congr_arg succ _ pattern), Lean isn't able to unify the successor case as it is with nat. Is there any way to get Lean to say what it's using behind the scenes to solve the unification problem? None of the definitions in core or init that are tagged with attributes jumped out as an obvious culprit.

#### Floris van Doorn (Jul 31 2019 at 23:21):

I think this attribute is the culprit: https://github.com/leanprover-community/lean/blob/master/library/init/core.lean#L417

#### Floris van Doorn (Jul 31 2019 at 23:21):

This works for me:

inductive mynat
| zero : mynat
| succ (n : mynat) : mynat

namespace mynat

protected def add : mynat → mynat → mynat
| a zero     := a
| a (succ b) := succ (add a b)

instance : has_zero mynat := ⟨mynat.zero⟩
instance : has_one mynat := ⟨mynat.succ mynat.zero⟩

lemma succ_add : ∀ n m : mynat, (succ n) + m = succ (n + m)
| n 0     := rfl
| n (m+1) := congr_arg succ (succ_add n m)

end mynat


#### Floris van Doorn (Jul 31 2019 at 23:24):

Oh, actually, when I remove the [pattern] attribute this example still works...

#### Chris B (Jul 31 2019 at 23:57):

Thank you, you're a hundred percent right and I am every bad adjective in the book.I made a completely stupid mistake and defined add as add ((succ a) b) and proceeded to totally ignore it while putting everything else under the microscope. My apologies.

#### Floris van Doorn (Aug 01 2019 at 00:38):

No problem! If you make a mistake it is very hard to figure out where exactly the mistake is.

Last updated: May 12 2021 at 04:19 UTC