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

[PVS-Help] function domains

To: pvs-help@csl.sri.com
Subject: [PVS-Help] function domains
From: "R. Colvin" <robert@itee.uq.edu.au>
Date: Fri, 14 May 2004 14:18:33 +1000
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

Is it possible to extract the domain of a function?  Eg, given 

f: [T1 -> T2] = ...

the expression f`domain returns the set T1.  Similarly for

f: [{t: T1 | p(t)} -> T2] = ...

the expression f`domain returns the set {t: T1 | p(t)}.  

Thanks,
Rob

Prev by Date: Re: [PVS-Help] singleton lists
Next by Date: [PVS-Help] PP algorithm theories
Prev by thread: Re: [PVS-Help] PP algorithm theories
Next by thread: Re: [PVS-Help] function domains
Index(es):
- Date
- Thread