coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Math Prover <mathprover AT gmail.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] record value of "destruct" tactic
- Date: Fri, 31 May 2013 19:57:23 -0700
Hi!
This is a minimal test case of a problem I'm running into.
Often, when I do "destruct [big complicated _expression_]", I would like to have a hypothesis of the form:
H: [big complicated _expression_] = value1
The reason this shows up is that often I destruct _expression_, but then later, when I unfold another _expression_, I need access to the initial destructed _expression_. Thus, my question: is there a way to do something like "destruct expr; but also remember that expr = ... as a hypothesis"
Thanks!
Attachment:
fail.v
Description: Binary data
- [Coq-Club] record value of "destruct" tactic, Math Prover, 06/01/2013
- Re: [Coq-Club] record value of "destruct" tactic, Gabriel Scherer, 06/01/2013
- Re: [Coq-Club] record value of "destruct" tactic, Math Prover, 06/01/2013
- Re: [Coq-Club] record value of "destruct" tactic, AUGER Cédric, 06/03/2013
- Re: [Coq-Club] record value of "destruct" tactic, Math Prover, 06/01/2013
- Re: [Coq-Club] record value of "destruct" tactic, Gabriel Scherer, 06/01/2013
Archive powered by MHonArc 2.6.18.