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

Re: [PVS-Help] A representation of symbols in PVS


Since the type system is open-ended, there isn't a way to define
a type that is the disjoint union of all types.  You can only do this
for a fixed collection of types.  Using a type parameter gives you some
flexibility in that it can be instantiated with a newly defined
type, but even this is limited since the new type can't be recursive
in the data type.  It might be useful to discuss what you're trying to
formalize so that we can figure out a good way to achieve it.  


Aaron W. Hsu <arcfide@sacrideo.us> wrote:

> Hrm, on further evaluation, using the symbol type is useful, but now I
> have encountered another issue. I'd like for my expressions to contain
> any random elements of any type. That is, more than just symbols, I
> would like my s-expressions to contain numbers as well, for example. Is
> there a way of making a sort of generic type so that I can go through an
> s-expression and potentially obtain any sort of value?