What does the syntax [className x] mean

Stream: lean4

[Jafar Tanoukhi]

While reading through Mathlib I noticed this syntax in Mathlib/Data/Fintype/Defs.lean.

variable {α β γ : Type*}
-- code here
variable [Fintype α]
-- other code here

What does this do exactly? I'm not very sure I understand classes other than the basics that you can make instances of it; to support ad-hoc polymorphism. Isn't α already declared too ?

[Jafar Tanoukhi]

"I asked this here and not in the mathlib channel, as it is more related to the syntax of lean4 than the fact that this was found in mathlib."

[Aaron Liu]

It means to synthesize the instance of Fintype α automatically by typeclass

[Aaron Liu]

when using theorems

[Aaron Liu]

so if you have

theorem exists_const {b : Prop} (α) [i : Nonempty α] : (∃ _ : α, b) ↔ b :=
  ⟨fun ⟨_, h⟩ => h, i.elim Exists.intro⟩

then you can use it as exists_const Nat and it will fill in [i : Nonempty Nat] automatically

[Kenny Lau]

@Jafar Tanoukhi you might want to refer to TPIL Ch. 10

[Jafar Tanoukhi]

Sorry I disappeared, was trying to understand the answer. But i'm not sure I do.

[Jafar Tanoukhi]

Wouldn't lean know to replace α with Nat without the whole Fintype α variable syntax ?

[Jafar Tanoukhi]

Kenny Lau said:

Jafar Tanoukhi you might want to refer to TPIL Ch. 10

Alright I will, thanks.