[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Parameter type resolution
How can I make types I define in a given theorem available as types of
parameters to other theorems? For example:
my_types: THEORY BEGIN
R: TYPE = real
END my_types
my_thms[p: R]: THEORY BEGIN
% ...
END my_thms
When trying to validate this code, the typechecker complains that
there is "No resolution for R." Why is it that I'm able to use other
types defined within theories with no problem; for example, 'posnat'
and 'real'? (How) Can I take advantage of those same facilities to
make the above code work? Thanks
jerome