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

Re: [PVS-Help] Parameter type resolution

You have to import the theory, e.g.,

my_thms[(IMPORTING my_types)
        p:R] : THEORY
BEGIN
  ..
END my_thms

Cesar
Jerome wrote:
> 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
> 
> 

-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@xxxxxxxxxx
National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4