lean4 version of `retrieve`?

Stream: lean4

[Thomas Murrills]

Is there one of the following:

1. a lean4 version of retrieve which lets me run tactics and change the mvar context, then reset it when I'm done
2. a standard workaround for retrieve
3. a general pattern that achieves the same effect as the following: "duplicate" a metavariable with all of its local context, act on the duplicate in TacticM, then extract some info from it and throw the duplicate metavariable away.

I can do the last one manually via mkFreshExprMVarAt etc., but it seems a bit hacky.

Ideally I'd like no record of what I did besides the info I extract, so I'm also not sure if there are cache and other "monad-persistent" details to worry about. (is saveState/restoreState sufficient to take care of everything?)

Thanks!

[Mario Carneiro]

saveState and restoreState are probably what you want here

[Mario Carneiro]

I think there is a function in MonadBacktrack that does the equivalent of retrieve too

[Mario Carneiro]

probably you want either withoutModifyingState or observing?

[Thomas Murrills]

Thanks, withoutModifyingState looks like it's what I need! :)