Investigating `abbrev`

Stream: general

[Asei Inoue]

I want to gain a better understanding of what abbrev does.

abbrev NaturalNumber := Nat
#check (2 : NaturalNumber)

Is there a way to examine how this code is interpreted by Lean, and why it doesn’t result in an error?

[Kenny Lau]

@Asei Inoue abbrev means that "when you're doing typeclass search, unfold this". For example, for the notation + to work on a type α, you first need to provide an instance of Add α. If you now have def Test := α and try to do + on Test; it wouldn't work, because the typeclass search can't figure out the instance of Add Test; but if you do abbrev Test := α instead, then the typeclass will unfold Add Test to Add α, and will then successfully find the instance.

[Kenny Lau]

Code:

variable (α : Type u) [Add α]
#check fun (x y : α) ↦ x + y       -- control

def Test := α
#check fun (x y : Test α) ↦ x + y  -- failed to synthesize HAdd (Test α) (Test α) ?m.154

abbrev Test' := α
#check fun (x y : Test' α) ↦ x + y -- succeeds

[Asei Inoue]

Is there a way to verify in Lean code that type class resolution looked for an instance of Add α rather than Add Test?

[Kenny Lau]

@Asei Inoue
image.png

If you put your text cursor on the #check and click on the x + y in the infoview and keep clicking, this is what you will see

[Kenny Lau]

Lean synthesised HAdd (Test' α) (Test' α) (Test' α) from the instance of Add α.

[Asei Inoue]

nice!

[Asei Inoue]

thank you very much!