[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