[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.