[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Parametrized type equivalence
Dear PVS Developers/Users,
I have a question respect to the parametrization of types.
There are two theories:
A[T: TYPE] defines a type called AT which depends on T
B[T: TYPE]: THEORY
a1: VAR AT
a2: VAR AT[T]
Are the types of the of a1 and a2 variables equivalent? I think, yes;
...because a2 is an instance of AT with parameter T, but in the end both
of the variables are "generic" having a parameter T:TYPE. Can somebody
confirm this assumption?
Thank you very much!