Zulip Chat Archive

Stream: general

Topic: implicit parameters of structure/class fields

view this post on Zulip Reid Barton (Nov 26 2018 at 15:42):

Are the rules for the types of the field accessors (in particular, whether arguments are explicit or implicit) written out somewhere (not in C++)?

view this post on Zulip Keeley Hoek (Nov 26 2018 at 23:58):

I don't fully know what you mean Reid, so sorry if this stuff you already know, but given struct : name and field : name you can infer the type of the honest function named struct and of the projection struct ++ field, then unwind the Pi binders off the projection which just correspond to the type arguments passed to struct. That's how I've figured out what all the arguments are and what their binder_info is in the past.

Last updated: May 14 2021 at 13:24 UTC