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

[PVS-Help] how to use "list" which is in pvs prelude

To: pvs <pvs-help@xxxxxxxxxxx>
Subject: [PVS-Help] how to use "list" which is in pvs prelude
From: applehopedream <applehopedream@xxxxxxx>
Date: Sun, 11 May 2008 10:11:34 +0800 (CST)
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@xxxxxxxxxxx

I want to use a list with a certain length and certain elements ,but I don't know how to set the length and elements.

杭州复地连城国际地铁生活方式，76-134㎡精品房源热销中

Prev by Date: Re: [PVS-Help] rewriting add_as_union
Next by Date: [PVS-Help] PVS 4.1 Errors
Prev by thread: Re: [PVS-Help] PVS 4.1 Errors
Next by thread: Re: [PVS-Help] how to use "list" which is in pvs prelude
Index(es):
- Date
- Thread