[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] About Datatypes and Codatatypes
I was reading through the presentation "Coalgebras in PVS" (http://www.csl.sri.com/users/owre/slides/wg1-3-coalgebras/
) and noticed that it is mentioned that some of the restrictions over datatype definition are overly restrictive. For example, we can't use finite sets, which I was trying to use in an recursive reference in an accessor. Do you have any plans on improving these restrictions in the near future?
Also, I read about the codatatypes and the bisimulation relation. I understood that this would help in overcoming such restrictions, but I have been unable to use it with finite sets as well. Have I got it wrong? :-)
Do you happen to know any definitions of a multiset theory using datatypes or codatatypes? I would be interested on that. I found some theories that define it using predicates (multiset: TYPE = [T -> nat]), similarly to the set definition in the prelude. However, this is not allowed to use when defining the datatype.