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

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


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.


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

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