coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Feature request

From: Kate and James Candy <jacinabox AT hotmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Feature request
Date: Wed, 23 Apr 2014 10:30:56 +0000

Lately I've been wishing for a smarter pattern tactic, that can be made to do
its work in a subterm of the goal. For example, if the goal is (P (x ^ 2 *
exp x)), I could do pattern2 (x ^ 2) x and get the goal (P ((fun x => x ^ 2)
x * exp x)).

--jacinabox

[Coq-Club] Feature request, Kate and James Candy, 04/24/2014
- Re: [Coq-Club] Feature request, Cedric Auger, 04/24/2014
  - Re: [Coq-Club] Feature request, Jason Gross, 04/24/2014