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

[PVS-Help] A representation of symbols in PVS

I am attempting to create some sort of "symbol" type for use in an
s-expression datatype. 

Basically, I want to do transformations on these s-expressions of
symbols. I need some sort of data type that has equality of two symbols
that are the same, such as (eq? 'a 'a). I know that I could use
enumerated types, but this restricts the functions in some way to a
limited set of symbols. Is there some way to define a datatype of
symbols where the number of symbols is infinite, or do I have to
enumerate all the symbols I am going to use ahead of time and work with
it this way? 

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))) ++++++++++++++