coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct
Chronological Thread
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct
- Date: Sat, 24 Jan 2015 00:11:17 -0800
Hi,
In case others may find this discovery interesting (if you have not already made it yourselves):
It is possible to mostly eliminate the verbose [match goal with ... end] construct in trunk/8.5 by using the following tactic:
Ltac hyp := multimatch goal with H : _ |- _ => constr:H end.
Note that [let H := hyp in ... ] will automatically backtrack across failures of subsequent tactics, due to [multimatch]:
Goal False -> True -> False -> True.
intros.
let H := hyp in exact H.
Using open_constr and uconstr tactic notations, I presume the other features of match (pattern matching on the body and the type) can be duplicated with shorter syntax, too.
-Jason
- [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jason Gross, 01/24/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/24/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Emile Lunardon, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jason Gross, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/27/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/26/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jason Gross, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Emile Lunardon, 01/25/2015
- Re: [Coq-Club] Globally-nameless tactics: Getting rid of the verbose Ltac [match goal with] construct, Jonathan Leivent, 01/24/2015
Archive powered by MHonArc 2.6.18.