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

To: pvs-help <pvs-help@csl.sri.com>
Subject: [PVS-Help] about the definition of a special TYPE
From: "Wei K Mr (PG/R - Computing)" <K.Wei@surrey.ac.uk>
Date: Wed, 27 Oct 2004 02:34:40 +0100
List-Help: <mailto:pvs-help-request@csl.sri.com?subject=help>
List-Id: PVS-Help <pvs-help.csl.sri.com>
List-Post: <mailto:pvs-help@csl.sri.com>
List-Subscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>
List-Unsubscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>
Sender: pvs-help-bounces+archive=csl.sri.com@csl.sri.com
Thread-Index: AcS7xSCfUzbj08H9SPuCnXX/PKRouw==
Thread-Topic: 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