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

[PVS-Help] Simple PVS setup question



Hi,

I followed all of the instructions to install PVS on
my machine and am running into the following problem
(I haven't modified the pvs script or anything):

I have a file, ex1.pvs that consists of the following:
ex1: THEORY

BEGIN

f(x:nat):nat=x+1

END ex1

I do M-x tc and get the following message:
/home/<user>/pvs-3.2/Examples/ex1.pvs is not in the
current context

Any suggestions? Thanks a lot.

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com