Zulip Chat Archive

Stream: new members

Topic: explicit parameter in inductive constructor


view this post on Zulip Horatiu Cheval (Apr 08 2021 at 11:12):

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?

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 11:36):

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

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

view this post on Zulip Horatiu Cheval (Apr 08 2021 at 11:48):

Thanks! That's what I needed.

view this post on Zulip Horatiu Cheval (Apr 08 2021 at 11:52):

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?

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 11:54):

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

view this post on Zulip Horatiu Cheval (Apr 08 2021 at 12:00):

Yeah, I guess I was going too far :)

view this post on Zulip Kevin Buzzard (Apr 08 2021 at 12:00):

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.

view this post on Zulip Mario Carneiro (Apr 09 2021 at 01:47):

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 01:48):

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


Last updated: May 13 2021 at 06:15 UTC