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

Re: [PVS-Help] Supertype

Hi Yuzhang,

It is not possible to create a supertype that contains
incompatible types, but it is possible to create a sum type,

If you are using PVS 3.0 or later, "[int + string]" is a disjoint
sum type that in a sense contains both integers and strings.  See
cotuples in the new features of the PVS 3.0 release notes for
details (M-x pvs-release-notes).

In earlier versions you need to use the union type from the


> From:    Feng Yuzhang <fengyuzh@comp.nus.edu.sg>
> Subject: [PVS-Help] Supertype
> Date:    Tue, 23 Dec 2003 17:29:36 +0800 (GMT-8)
> To:      pvs-help@csl.sri.com
> Hi there,
> I would like to ask whether it is possible to define a supertype of some
> pre-defined types, eg. a type called "datavalue" of which integers and
> strings are subtype.
> Thanks
> Yuzhang
> School Of Computing
> National University of Singapore