withMainContext

Stream: mathlib4

[Yury G. Kudryashov]

In this code, I'm using replaceMainGoal inside of withMainContext. After that, FVarIds in a previously elaborated Expr are no longer valid. How should I deal with this?

[Yury G. Kudryashov]

To re-elaborate prf, I need to repeat instance search (because the Syntax may fail to elaborate without type information)

[Yury G. Kudryashov]

Or should I get the variable name from the old context, then find a variable with the same name in the new context?

[Scott Morrison]

This is not specific to your code / question, but I've found that writing tactics in TacticM is highly error prone, and that it's better to first write functions in MetaM (i.e. that explicitly receive and return MVarIds), and only in a very simple outer function do goal management.

[Scott Morrison]

(Of course, this means you suffer when you find that people have written tactics at the TacticM level, or only with Syntax consuming interfaces, when you want them down at MetaM...)

[Yury G. Kudryashov]

I guess, Context may be necessary for a tactic that wants to output meaningful error messages.

[Yury G. Kudryashov]

(e.g., mention a particular line/char that makes the tactic unhappy)