The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hi, Jason --

That is producing the right term but it requires a lot of goal manipulation and I haven't found a good way use those kinds of tactics to construct the term that I want and then return them to be used by other tactics. 

On Tue, Sep 3, 2013 at 5:57 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Does [let x := fresh in set (x := bar); try revert x] do what you want?

-Jason

On Tuesday, September 3, 2013, Gregory Malecha wrote:

Hello --

I have a term [foo] with a lot of occurances of a large subterm [bar]. I would like to abstract all of the instances of [bar] and produce a term like:

let x := bar in foo[bar |-> x]

One way to do something like this is with the [pattern] tactic, but this fails when there is dependency on [bar] since it is constructing a lambda abstraction, i.e. it constructs:

(fun x =>  foo[bar |-> x]) bar

I have a plugin/patch that achieves the former but I am wondering if there is an existing way to do it that I don't know about.

Thank you very much.

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/