Context after in tactic_code_action

Stream: batteries

[Patrick Massot]

When defining a tactic_code_action, is there a convenient way to run some MetaM code in the context that come after applying the tactic?

[Patrick Massot]

Oops, I just saw Yannis asked the question with more details at #mathlib4 > tactic_code_action find the context after the execution of t @ 💬 . Sorry about the duplicate post.