Zulip Chat Archive

Stream: mathlib4

Topic: withMainContext


Yury G. Kudryashov (Nov 27 2022 at 02:08):

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 (Nov 27 2022 at 02:10):

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

Yury G. Kudryashov (Nov 27 2022 at 02:10):

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 (Nov 27 2022 at 02:40):

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 (Nov 27 2022 at 02:41):

(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 (Nov 27 2022 at 07:34):

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

Yury G. Kudryashov (Nov 27 2022 at 07:34):

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


Last updated: Dec 20 2023 at 11:08 UTC