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

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


Thank you for your message...

On 24-Mar-2009 Natarajan Shankar wrote:

> The simplest thing would be to define a datatype with a
> single constructor "symbol" with an accessor name of type string
> which is defined in the PVS prelude.  Another option is to leave
> the symbol type as a type parameter that is instantiated as needed.
> The choice depends on how you plan to use the data type.

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?

Aaron W. Hsu <arcfide@sacrideo.us> | <http://www.sacrideo.us>
"Government is the great fiction, through which everybody endeavors to
live at the expense of everybody else." -- Frederic Bastiat
+++++++++++++++ ((lambda (x) (x x)) (lambda (x) (x x))) ++++++++++++++