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

Re: [PVS-Help] error in importing theory


Without seeing your specs I can only guess what might be going on here.

The PVS importing is for theories, not files.  Hence if your file name is
impl__min__min.pvs, but it specifies theories foo and bar, you will get
the error you see.  In this case you should change to 'importing foo, bar'.

If that is not the issue, could you please send me your files so I can see
what is going on?

Sam Owre

masoome parsa <masoome.parsa@xxxxxxxxx> wrote:

> Hi,
> I have a pvs file with a theory that imports another file. When I use type
> checking for this theory , it gives me this error :
> Can't find file for theory impl__min__min
> In my pvs file I have this line of code : importing impl__min__min
> Anybody knows how I can fix this error !?
> Thank you.