Stream: Coq users

Topic: ✔ Is it possible to generalize multiple vars in a single ...


view this post on Zulip Daniel Hilst Selli (Dec 29 2021 at 02:40):

I'm doing generalize dependent a. generalize dependent b is there anything like generalize dependent a, b?

view this post on Zulip Li-yao (Dec 29 2021 at 03:20):

There's revert a b although you have to also mention the hypotheses that depend on those variables, and otherwise you can define your own tactic Ltac gd2 a b := generalize dependent a; generalize dependent b.

view this post on Zulip Daniel Hilst Selli (Dec 29 2021 at 17:37):

Hmm a custom tactic is a good idea, thank you!


Last updated: Feb 04 2023 at 22:29 UTC