[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] singleton_elt
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 <email@example.com> wrote:
> example[T: TYPE, f: FUNCTION[T -> T]]: THEORY
> IMPORTING operator_defs_ext[T]
> g(a, b: T): T = f(union(a, b))
> ident: LEMMA identity?(g)(emptyset)
> END example