Re: [PVS-Help] singleton_elt

[Natarajan Shankar <shankar@xxxxxxxxxxx>]

Jerome: I think the way you have it with T as a parameter and
f and g declared over set[T] is the best approach.  Otherwise,
you'd have to say that T is a subtype of set[T] that is closed with
respect to operations like union, interection, and complement.
That can be done, but it might be more complicated than you want.

-Shankar

Jerome White <jerome@cs.caltech.edu> wrote:

Jerome White <jerome@cs.caltech.edu> wrote:

> 
> Thanks Shankar. When I alter the definition of 'f' and 'g' as such
> 
>   f: FUNCTION[set[T] -> set[T]]
>   g(a, b: set[T]): set[T]
> 
> the singleton_elt's go away. I take it my mistake was in thinking that
> PVS knew T was a set. Is there any way I can express that in the
> parameterized type definition? Something like the following
> 
>   example[T: TYPE FROM set, f: FUNCTION[T -> T]]: THEORY
> 
> I realise this isn't correct, but that's the gist.
> 
> jerome