coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] pattern tactic that generates [let...in...], Gregory Malecha, 09/03/2013
- <Possible follow-up(s)>
- [Coq-Club] Pattern tactic that generates [let...in...], Gregory Malecha, 09/03/2013
- Re: [Coq-Club] Pattern tactic that generates [let...in...], Jason Gross, 09/03/2013
- Re: [Coq-Club] Pattern tactic that generates [let...in...], Gregory Malecha, 09/04/2013
- Re: [Coq-Club] Pattern tactic that generates [let...in...], Jason Gross, 09/04/2013
- Re: [Coq-Club] Pattern tactic that generates [let...in...], Gregory Malecha, 09/04/2013
- Re: [Coq-Club] Pattern tactic that generates [let...in...], Jason Gross, 09/03/2013
Archive powered by MHonArc 2.6.18.