[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
(forall (t: T): P1 implies P2)
(provided t is not free in P2)
Or is there some other way?