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

Regards,
Sam

> 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