explicit parameter in inductive constructor

Stream: new members

[Horatiu Cheval]

When I define something like this

inductive prf (a : list ℕ) : ℕ → Type
| mk1 (n : ℕ) : prf (n + n)
#check @prf.mk1
-- prf.mk1 : Π {a : list ℕ} (n : ℕ), prf a (n + n)

a is an implicit argument in the constructor, even if I have it explicit in the inductive definition.
Can I make it so that a is generated as explicit in prf.mk1?

[Kevin Buzzard]

I've never really understood why, but I think the syntax nowadays is

inductive prf (a : list ℕ) : ℕ → Type
| mk1 [] (n : ℕ) : prf (n + n)

[Horatiu Cheval]

Thanks! That's what I needed.

[Horatiu Cheval]

Now I wonder, if you have several arguments, can you specify some of them to be implicit and some to be implicit?

inductive prf (a : list ℕ) (b : bool) : ℕ → Type
| mk1 [] (n : ℕ) : prf (n + n)
#check @prf.mk1
-- prf.mk1 : Π (a : list ℕ) (b : bool) (n : ℕ), prf a b (n + n)

Both a and b are explicit, and without the [] they are implicit. Is there a syntax for, let's say, a to be implicit and b to be explicit?

[Kevin Buzzard]

Beyond some point you just might want to make your own constructor rather than getting the equation compiler to do it for you :-)

[Horatiu Cheval]

Yeah, I guess I was going too far :)

[Kevin Buzzard]

Actually I think your question is reasonable, and there might be a way to do it -- I'm not an expert in inductive types, I only ever use structures.

[Mario Carneiro]

No, there is not much ability to change the binders beyond the {} [] setting shown here

[Mario Carneiro]

But like Kevin says you can mostly paper over this by defining your own constructors. You will see a lot of structure fields in mathlib have primed names for this reason