De-surgaring Type classes and instances

Stream: new members

[Rajiv]

I am currently reading through Section 10.1 of Theorem Proving with Lean (https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#type-classes-and-instances)

I was wondering if the following intuition of mine, regarding how de-suraging of Type class and instance declaration works in Lean is correct?

If there is something that I might be missing out in my understanding please let me know.

It looks like Type classes are not yet documented in Lean Reference Manual, so the only resource seems to be Theorem Proving in Lean.

universe u

class inhabited₁ (α : Type u) :=
  (default : α)

@[class]
structure inhabited₂ (α : Type u) :=
  (default : α)

attribute [class]
structure inhabited₃ (α : Type u) :=
  (default : α)

instance nat_inhabited₁ : inhabited₁ nat :=
  inhabited₁.mk nat.zero

instance nat_inhabited₂ : inhabited₂ nat :=
  ⟨nat.zero⟩

def nat_inhabited₃ := @inhabited₃.mk nat nat.zero

attribute [instance]
nat_inhabited₃