Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Slow QED

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Slow QED


Chronological Thread 
  • From: Thomas Braibant <thomas.braibant AT gmail.com>
  • To: Kenneth Roe <kendroe AT hotmail.com>
  • Cc: Coq-Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Slow QED
  • Date: Mon, 22 Apr 2013 22:07:44 +0200

> Thanks. I actually thought about using "vm_compute." The problem is that I
> have many goals that look like the following:
>
> ?86 = simplify (...)
>
> "simplify" is a fixpoint that does some sort of simplification on a complex
> term such as a program AST. What I would like to do is evaluate the rhs
> term and then instantiate the variable ?86 with the result. The problem is
> that "vm_compute" does not work with existentials. Is there a trick for
> working around this issue?
>
> - Ken

If you re read my previous response, you will see that I mention such
a trick to use vm_compute with evars, through the use of a dedicated
plugin for Coq ;).

Cheers,
Thomas



Archive powered by MHonArc 2.6.18.

Top of Page