Omitting indexing type in a pi type

Stream: mathlib4

[Yaël Dillies]

What's the Lean 4 syntax to omit the type of the indexing type of a pi type?

[Scott Morrison]

Can you show the Lean 3 syntax? I don't understand the question yet.

[Eric Wieser]

Π a : α, β a is to Π a, β a as (a : α) → β a is to ...?

[Moritz Doll]

(a : _) → β a works, but it is not really nice

[Yaël Dillies]

Oh, is it just \forall a, \beta a by any chance?

[Moritz Doll]

that seems to work as well