Zulip Chat Archive

Stream: new members

Topic: what's in an environment?

Yasmine Sharoda (Dec 02 2020 at 17:12):

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 (Dec 02 2020 at 17:36):

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

Reid Barton (Dec 02 2020 at 17:36):

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

Reid Barton (Dec 02 2020 at 17:38):

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 (Dec 02 2020 at 17:41):

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 (Dec 02 2020 at 19:27):

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 (Dec 02 2020 at 19:33):

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

Reid Barton (Dec 02 2020 at 19:34):

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 (Dec 02 2020 at 19:36):

exactly what I am looking for.. thank you

Last updated: Dec 20 2023 at 11:08 UTC