Huỳnh Trần Khanh (Oct 12 2022 at 15:05): Huỳnh Trần Khanh (Oct 12 2022 at 15:05):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.
Gaëtan Gilbert (Oct 12 2022 at 15:07):Check S ltac:(exact 0).
Théo Zimmermann (Oct 12 2022 at 15:16):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.
Notification Bot (Oct 13 2022 at 00:11):Huỳnh Trần Khanh has marked this topic as resolved.
Last updated: Sep 30 2023 at 05:01 UTC