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++)?
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