Re: [PVS-Help] singleton_elt

[Natarajan Shankar <shankar@xxxxxxxxxxx>]

Jerome:

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-.

-Shankar

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