why eq.refl has type eq a a?

Stream: general

[Coriver Chen]

In https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#inductive-families, the eq inductive family is defined as

inductive eq {α : Sort u} (a : α) : α → Prop
| refl [] : eq a

I don’t understand why eq.refl has type eq a a. Isn’t it just eq a?

[Kevin Buzzard]

The second a is the one before the colon in the first line. You don't write it on the second line because it's automatically inserted whilst making the definition, but #check eq.refl shows you it's there.

[Kevin Buzzard]

I also remember being totally confused by this at exactly the same point :-)

[Coriver Chen]

yeah. Quite confusing in a first look. It seems the first a is the one appeared in first line

[Coriver Chen]

If I change it to

inductive eq {α : Sort u} (a : α)  (b : α) : α → Prop
| refl [] : eq a

I get eq a b a. Knowing this rule it makes sense now

[Kevin Buzzard]

I think it changed in Lean 4 so be careful out there :-)

[Coriver Chen]

https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html Ah indeed, it changed to Eq a a