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

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

To: "Wei K Mr (PG/R - Computing)" <K.Wei@surrey.ac.uk>
Subject: Re: [PVS-Help] about the definition of a special TYPE
From: Hendrik Tews <tews@tcs.inf.tu-dresden.de>
Date: Wed, 27 Oct 2004 13:00:50 +0200
Cc: pvs-help <pvs-help@csl.sri.com>
In-Reply-To: <A59EC876DF4FEB439771FDDD7E3C72CB4FB207@EVS-EC1-NODE1.surrey.ac.uk>
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>
References: <A59EC876DF4FEB439771FDDD7E3C72CB4FB207@EVS-EC1-NODE1.surrey.ac.uk>
Sender: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

Wei K Mr (PG/R - Computing) writes:
    
   Is it possible to define a TYPE which contains all natural
   numbers and a special element, tick?
    
How about lift[nat]? Or you define your own datatype with tick
instead of bottom.

Bye,

Hendrik

References:
- [PVS-Help] about the definition of a special TYPE
  - From: "Wei K Mr (PG/R - Computing)" <K.Wei@surrey.ac.uk>

Prev by Date: [PVS-Help] about the definition of a special TYPE
Next by Date: [PVS-Help] Proof Tree
Prev by thread: [PVS-Help] about the definition of a special TYPE
Next by thread: [PVS-Help] Parsing after changing imported theory
Index(es):
- Date
- Thread