coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Ltac and constr arguments with holes
- Date: Mon, 10 Nov 2014 00:54:18 +0100
Arnoud, Jonathon: thanks for the replies.
Inspired by Jason's message on splitting evars, I ended up with
Tactic Notation "my_destruct" open_constr(z) :=
match goal with
| _ : context [?z'] |- _ => unify z z'; destruct z
end.
Goal forall x, 1 + 2 = x -> True.
intros.
my_destruct (_ + _).
Restart.
intros.
my_destruct (1 + _).
auto.
auto.
Qed.
This seems to work, even on Coq 8.4.
On 11/06/2014 01:38 PM, Robbert Krebbers wrote:
Tactics like destruct accepts terms with holes for their arguments. For
example:
Goal forall x, 1 + 2 = x -> False.
intros.
destruct (1 + _) eqn:?.
Abort.
Here, I am allowed to put an "_" instead of the 2, and Coq will infer
it. Especially if one has to deal with very large terms, this is
extremely useful.
Now I want to use destruct as part of an Ltac tactic, and be able to use
underscores in arguments to the Ltac tactic as well. However, that does
not seem to work:
Ltac my_destruct z := destruct z eqn:?.
Goal forall x, 1 + 2 = x -> False.
intros.
Fail my_destruct (1 + _).
(* Cannot infer this placeholder. *)
Abort.
I tried to play around with tactic notation, but without luck:
Tactic Notation "my_destruct_alt" open_constr(z) := destruct z eqn:?.
Goal forall x, 1 + 2 = x -> False.
intros.
my_destruct_alt (1 + _).
(* Now I have a meta in Heqn *)
Abort.
Any suggestions?
- [Coq-Club] Ltac and constr arguments with holes, Robbert Krebbers, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Arnaud Spiwack, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/07/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/07/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/07/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Robbert Krebbers, 11/10/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/10/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jason Gross, 11/10/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/10/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Arnaud Spiwack, 11/06/2014
Archive powered by MHonArc 2.6.18.