Dear Aaron W. Hsu: I think you can use "choose" function. These is an example which may be helpful for you. ----- Original Message ----- From: "Aaron W. Hsu" <arcfide@sacrideo.us> To: "Natarajan Shankar" <shankar@csl.sri.com> Cc: <pvs-help@csl.sri.com> Sent: Tuesday, March 24, 2009 11:50 PM Subject: Re: [PVS-Help] A representation of symbols in PVS > Natarajan, > > 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))) ++++++++++++++ > >
On the Verification of VDM Specification and Refinement withPVS.pdf