Stream: Coq users

Topic: ✔ Redefining a built-in tactic

view this post on Zulip Meven Lennon-Bertrand (Feb 16 2023 at 14:12):

Is there a way to redefine a built-in tactic? Concretely, I tried the following:

Ltac refold := idtac "foo".

Ltac core_constructor := constructor.
Ltac constructor ::= core_constructor ; refold.

Goal nat.
constructor. (* does not print anything… *)

But it seems like constructor does not get redefined as I hoped it would be…

view this post on Zulip Gaëtan Gilbert (Feb 16 2023 at 14:15):

Tactic Notation "constructor" := core_constructor ; refold.

view this post on Zulip Notification Bot (Feb 16 2023 at 14:17):

Meven Lennon-Bertrand has marked this topic as resolved.

Last updated: Oct 04 2023 at 20:01 UTC