[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Using the PVS ground evaluator

Sam Owre wrote:

>I'm including all the fixed functions
>below.  Just add them to your ~/.pvs.lisp file (creating it if
>necessary) and your examples should work.
>
Thanks Sam, works like a charm now.

Is it possible to map values from lisp back to the prover? If one wants to
expand a term completely, it would be nice to be able to use the ground
evaluator as a fast rewriting engine.
-- 
pertti