Zulip Chat Archive

Stream: new members

Topic: what's in an environment?


view this post on Zulip 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.

view this post on Zulip Reid Barton (Dec 02 2020 at 17:36):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yasmine Sharoda (Dec 02 2020 at 19:36):

exactly what I am looking for.. thank you


Last updated: May 06 2021 at 20:13 UTC