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

Re: [PVS-Help] loading files, indentation


On Wed, 14 Apr, John Rushby wrote:
: > Is there a way of telling pvs to load a particular .pvs file from
: > the command line?
: PVS just passes command line arguments to Emacs, so it's just the same
: as starting Emacs on a file: type "pvs filename"

When I do that emacs loads the file but PVS doesn't seem to
go into pvs-mode for that buffer.  I need to use 'M-x ff' (or
something similar) to load it as a pvs file

: However, the normal method of use is to start PVS when your machine
: boots, and to leave it running for months on end, so your question
: suggests you may be using PVS in some nonstandard way.  Maybe you need
: batch mode?  (See Chapter 5 of the system manual).

I'm running PVS on a PC which I switch off every night, so I need to
rerun PVS each day (when I use it).

On an unrelated topic, I have a sequent of the form:

(exists (t: T): P1)

The type T is a 'datatype', and I'd like to do induction on it, but
can't since it is in an existential quantifier.  I guess I want a
rule along the lines of

(exists (t: T): P1) implies P2
rewrites to
(forall (t: T): P1 implies P2)

(provided t is not free in P2)

Or is there some other way?