Skip to Content.
Sympa Menu

coq-club - [Coq-Club] record value of "destruct" tactic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] record value of "destruct" tactic


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page