implicit parameters of structure/class fields

Stream: general

[Reid Barton]

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

[Keeley Hoek]

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.