meta questions

Stream: general

[Yury G. Kudryashov]

Hi, what of the following is available in meta programs? I'm asking about a function running as a cmd, not inside a proof.

• list of available variables;
• list of open namespaces;
• current namespace?

Another question: can I add a proof of, e.g., monoid_hom.id or monoid_hom.comp_apply from a command without making definition-specific code much less readable?

[Kevin Buzzard]

You know about #where, of course.

[Johan Commelin]

And I think that recently this stuff got exposed. You might want to look at recent commits by Keeley to core

[Gabriel Ebner]

You mean Simon.

[Johan Commelin]

Ooh, I guess I do. Sorry @Simon Hudon

[Simon Hudon]

indeed :)

[Yury G. Kudryashov]

Thank you, I didn't know about #where. I'll look into its source to find out how it works.