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

[PVS-Help] about the definition of a special TYPE



Hello,
 
Is it possible to define a TYPE which contains all natural numbers and a special element, tick?
 
for example, E:TYPE = {1, 2, tick}, but I need a TYPE = nat + tick.
 
Could we define it in PVS?
 
Many thanks!
 
Kun