[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Regarding theory declarations
I have a theory
what is inside the theory is not relevant for the time being. Then I have
Ta: THEORY = theory1[Na,Pa]
Tb: THEORY = theory1[Nb,Pb]
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?