Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Pattern tactic that generates [let...in...]

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Pattern tactic that generates [let...in...]


Chronological Thread 
  • From: Gregory Malecha <gmalecha AT cs.harvard.edu>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Pattern tactic that generates [let...in...]
  • Date: Tue, 3 Sep 2013 17:52:07 -0400

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



Archive powered by MHonArc 2.6.18.

Top of Page