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

Re: [PVS-Help] singleton_elt

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.


On Wed, May 13, 2009 at 06:33:55PM -0700, Natarajan Shankar wrote:
>If you do "M-x ppe" on "example, you'll see that the
>PVS type checker has introduced a bunch of conversions
>to transform a and b into singleton sets for the union
>and to convert union(a, b) and emptyset into something of
>type T by extracting the singleton_elt.
>I'm not sure what you intend here but it is very likely that
>these conversions are masking a genuine type error.  You can
>turn off these conversions using CONVERSION-.
>Jerome White <jerome@cs.caltech.edu> wrote:
>>    example[T: TYPE, f: FUNCTION[T -> T]]: THEORY
>>    BEGIN
>>      IMPORTING operator_defs_ext[T]
>>      g(a, b: T): T = f(union(a, b))
>>      ident: LEMMA identity?(g)(emptyset)
>>    END example