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

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

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!