coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Slow QED, Kenneth Roe, 04/22/2013
- Re: [Coq-Club] Slow QED, Thomas Braibant, 04/22/2013
- RE: [Coq-Club] Slow QED, Kenneth Roe, 04/22/2013
- Re: [Coq-Club] Slow QED, AUGER Cédric, 04/22/2013
- Re: [Coq-Club] Slow QED, Thomas Braibant, 04/22/2013
- Re: [Coq-Club] Slow QED, Thomas Braibant, 04/22/2013
- Re: [Coq-Club] Slow QED, AUGER Cédric, 04/22/2013
- Re: [Coq-Club] Slow QED, Frédéric Besson, 04/23/2013
- RE: [Coq-Club] Slow QED, Kenneth Roe, 04/22/2013
- Re: [Coq-Club] Slow QED, Thomas Braibant, 04/22/2013
Archive powered by MHonArc 2.6.18.