How does intros after revert_all remember hypothesis names?

Stream: general

[Rishi Mehta]

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]

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]

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

[Johan Commelin]

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