coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Ltac and constr arguments with holes
- Date: Thu, 06 Nov 2014 21:54:20 -0500
On 11/06/2014 08:56 PM, Jonathan wrote:
Actually - it is possible (in the trunk) if one is willing to use a bit of a kludge involving refine, an evar, and eval:
Tactic Notation "my_destruct" uconstr(p) :=
let e := fresh in
refine (let e := p in _);
[shelve
|let v := eval hnf in e in
match goal with _ : context[?C] |- _ => unify v C; clear e; destruct C eqn:? end].
Goal forall x, 1 + 2 = x -> False.
intros.
my_destruct (1 + _).
-- Jonathan
Oh, sorry, that only handles patterns with a single hole. Simple fix to make it work for any number of holes:
Tactic Notation "my_destruct" uconstr(p) :=
let e := fresh in
refine (let e := p in _);
shelve_unifiable;
let v := eval hnf in e in
match goal with _ : context[?C] |- _ =>
unify v C; clear e; destruct C eqn:?
end.
Goal forall x, 1 + 2 = x -> False.
intros.
my_destruct (_ + _).
-- Jonathan
- [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.