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

Extension set declaration

Hello everyone,

I'm looking for help on using PVS with sets.

I would like to know how to instanciate sets defined in extension. For 
example :
how to translate this : mySet = {atom1, atom2, ..., atomN} in PVS ?

I've already tried something like :

TMySet: TYPE = {atom1,atom2,...atomN}
mySet: setof[TMySet]

But there is no assurance that mySet contains exactly {atom1, atom2, ... 
atomN}. It can only be a subset of it ...

Thanks for your help,