Syntax for constructor with explicit parameter

Stream: lean4

[Horațiu Cheval]

inductive Foo (n : Nat) where
| mk

#check Foo.mk
-- Foo.mk {n : Nat} : Foo n

The n parameter of Foo is an implicit argument in the mk constructor. Is there a way to say that I want it to be explicit? Other than making n an index of Foo and binding it explicitly in mk. In Lean 3 there was the [] syntax

inductive foo (n : nat)
| mk [] : foo

#check foo.mk
-- foo.mk : Π (n : ℕ), foo n

[Sebastian Ullrich]

Other than making n an index of Foo and binding it explicitly in mk.

There is nothing wrong with that, indices are automatically promoted to parameters where possible

[Horațiu Cheval]

Right, though I still prefer to write parameters before the colon, because I like how it's clear from the signature that they won't change throughout the definition, and you don't need to look at the constructors to learn that. Maybe I'm still more accustomed to Lean 3 though.