withSaveInfoContext

Stream: lean4

[Mario Carneiro]

What does docs4#Lean.Elab.withSaveInfoContext do? I've read the docstring and the code but I still have no idea what it is supposed to do.

Resets the trees state t₀, runs x to produce a new trees state t₁ and sets the state to be t₀ ++ (InfoTree.context Γ <$> t₁) where Γ is the context derived from the monad state.

Is there an example of how or why you would want to wrap something in withSaveInfoContext?

[Wojciech Nawrocki]

Nodes in the info tree use the innermost withContext ancestor when pretty-printing and so on, so you'd want to use this whenever you change the (local, and maybe metavar, i forget) context so that the info nodes produced with this change in effect refer to the correct context.