what's in an environment?

Stream: new members

[Yasmine Sharoda]

A docs#environment as documented contains declarations and notation defined so far.
Does this contain structures and type classes?
To give a bit of context, I am trying to introspect the components of a type class, i.e. access their names and types.

[Reid Barton]

I think you want docs#environment.structure_fields and docs#environment.projection_info then

[Reid Barton]

Some explanation: for a structure/type class, let's say group, the environment will of course contain the type constructor group itself

[Reid Barton]

The declaration group is just a top-level constant, though. The structure info is stored separately.
A class could technically be anything, but usually it's a structure. Then environment.structure_fields on the name group will produce a list of (the names of) the projections out of that structure.

[Reid Barton]

Then you can look up these projections in the environment to find out what the fields of the structure are, or use environment.is_projection (actually, I'm not sure now how much more useful this would be)

[Yasmine Sharoda]

This is very good start. I believe I am now missing information about the type of the declaration, which is not part of projection_info.
would it be part of docs#declaration ? Its documentation is not very clear to me.

[Reid Barton]

The source https://github.com/leanprover-community/lean/blob/ed6accfb611bbd28ef5b7e34361d2b58a366e2c9/library/init/meta/declaration.lean#L47 has more specific documentation

[Reid Barton]

group for example will be a cnst with the name group, one universe parameter u and type Type u -> Type u. is_trusted is false for meta definitions, probably you can ignore it.

[Yasmine Sharoda]

exactly what I am looking for.. thank you