names of types of fields of a structure

Stream: lean4

[Matthew Ballard]

Suppose I have the Name of a structure. Returning the names of the fields as projection functions is straightforward. If I want instead the names of the types that are being projected to, what is the shortest path to that?

[Kyle Miller]

You can get constant declaration with let some decl := (← getEnv).find? projectionName | unreachable!, and then you can do something like forallTelescope decl.type fun _ body => pure body.getAppFn.constName? to get an Option Name

[Matthew Ballard]

Thanks. That’s about where I was. I was surprised that this isn’t part of the StructureInfo