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

Re: subset relationship in types

No, I mean "subset".  For example:

set1 : TYPE = finite_set[T]
set2 : TYPE = finite-set[T]

I need to write an ASSUMPTION, such that any variable from type of set2
would be subset of any variable from type of set1.


On Fri, 14 Mar 2003, John Rushby wrote:

> > Is there any way to specify a type of finite_sets as a subset of another
> > type of finite_sets, or I have to come up with my own definitions?
> If you mean "..as a SUBTYPE of another type..." then the TYPE_FROM
> construction may be what you are looking for.
> John