Zulip Chat Archive

Stream: new members

Topic: De-surgaring Type classes and instances


view this post on Zulip Rajiv (Dec 13 2020 at 12:21):

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₃

Last updated: May 15 2021 at 02:11 UTC