Stream: Coq users

Topic: ✔ Term mode and tactic mode

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 12 2022 at 15:07):

Check S ltac:(exact 0).

view this post on Zulip 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.

view this post on Zulip Notification Bot (Oct 13 2022 at 00:11):

Huỳnh Trần Khanh has marked this topic as resolved.

Last updated: Jun 23 2024 at 23:01 UTC