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

[PVS-Help] Regarding theory declarations



Hi--

I have a theory

theory1[N:above(1),P:above(2)]: THEORY
BEGIN

......
......

END

what is inside the theory is not relevant for the time being. Then I have 
another theory

theory2[Na,Nb:above(1),Pa,Pb:above(2)]: THEORY
BEGIN

IMPORTING theory1

Ta: THEORY = theory1[Na,Pa]
Tb: THEORY = theory1[Nb,Pb]

......
......

END

I am in the process of migrating certain theories from PVS 2.3 to PVS 3.2. 
While theory2 typechecks in PVS 2.3, this exact same theory does not 
typecheck in PVS 3.2

The error that I get is

"Illegal reference to Na
May not use theory declarations with actuals or mappings that reference 
entities declared in this theory"

Is there a way to work around the problem such that the fix achieves the 
same purpose as above?

rgds
-Nikhil

---
http://engr.smu.edu/~nikhil