Does Coq have a way to switch between "term mode" and "tactic mode"? These two terms are from Lean. For example, when I use a lemma and I need to quickly supply a proof as an argument, I would love a way to do it inline.
Check S ltac:(exact 0).
It's not as powerful as what Lean has though, because when you use such "tactics in terms", you cannot step through the tactics to see the intermediate subgoals and you have to use ;
only if you need to combine several.
Huỳnh Trần Khanh has marked this topic as resolved.
Last updated: Sep 30 2023 at 05:01 UTC