Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Instantiating existential variables

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Instantiating existential variables


chronological Thread 
  • From: "Samuel E. Moelius III" <moelius AT cis.udel.edu>
  • To: muad <muad.dib.space AT gmail.com>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Instantiating existential variables
  • Date: Thu, 12 Mar 2009 17:18:22 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
muad wrote:
Often I find that:
  refine (let u1 := _ in let u2 := _ in f (exist _ x u1) u2).
works, but I don't know if it suits every situation.

Nice!

Now, why does this behave differently than ``refine (f (exist _ x _) _)''?

Sam



Archive powered by MhonArc 2.6.16.

Top of Page