Zulip Chat Archive

Stream: general

Topic: How does intros after revert_all remember hypothesis names?


Rishi Mehta (Aug 11 2022 at 16:43):

Hello,

I'm writing some tooling to interact with lean. In the middle of a proof, I want to clear all the local context, retrieve the main goal metavariable, and then reinstate the local context. I'm able to do this by first running revert_all, followed by intros, eg here. I'm a little bit confused about how the intros command is able to remember and reinstate the names of the hypotheses (eg g1 and g2 in this example). I'm quite new to lean - could anyone point me to some documentation or code that explains this?

Thanks
Rishi

Johan Commelin (Aug 11 2022 at 16:47):

If you look at the goal after revert_all, you will see that it uses the correct names after . So those names are stored in the expression that is your new goal. And that's where intros gets the names from.

Rishi Mehta (Aug 11 2022 at 16:52):

Thanks Johan. That explains the names k and l, but not the hypothesis names g1 and g2, no?

Johan Commelin (Aug 11 2022 at 16:54):

I think the same mechanism applies, even though the pretty-printer doesn't display those names to you.


Last updated: Dec 20 2023 at 11:08 UTC