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

[PVS-Help] About Datatypes and Codatatypes



Hello all, 

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. 

Thanks, 

Leopoldo Teixeira
lmt@xxxxxxxxxxx