coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Enrico Tassi <enrico.tassi AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] vm_compute and evars
- Date: Thu, 24 Jan 2013 19:41:40 +0100
On Thu, Jan 24, 2013 at 06:38:42PM +0100, Thomas Braibant wrote:
> The idea is that when you have a term [T] that contains evars, it is
> possible to transform [T] into a function [F] in which evars have been
> abstracted, applied to these evars
The ssreflect plugin does this all over the place, but the main
motivation is to pass around just a constr (no evar map is needed if the
term is evar free).
If you want to give a look, the function is called pf_abs_evars, but it is
really tricky code.
Cheers
--
Enrico Tassi
- [Coq-Club] vm_compute and evars, Thomas Braibant, 01/24/2013
- Re: [Coq-Club] vm_compute and evars, Chung-Kil Hur, 01/24/2013
- Re: [Coq-Club] vm_compute and evars, Thomas Braibant, 01/24/2013
- Re: [Coq-Club] vm_compute and evars, Chung-Kil Hur, 01/25/2013
- Re: [Coq-Club] vm_compute and evars, Thomas Braibant, 01/25/2013
- Re: [Coq-Club] vm_compute and evars, Chung-Kil Hur, 01/25/2013
- Re: [Coq-Club] vm_compute and evars, Thomas Braibant, 01/24/2013
- Re: [Coq-Club] vm_compute and evars, Enrico Tassi, 01/24/2013
- Re: [Coq-Club] vm_compute and evars, Thomas Braibant, 01/25/2013
- Re: [Coq-Club] vm_compute and evars, Chung-Kil Hur, 01/24/2013
Archive powered by MHonArc 2.6.18.