The Coq mailing list

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

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/