[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Extending the prelude?
The short answer is yes (see page 20, Section 2.4, of our tutorial in
f). Proveit supports this type of extensions.
The short question is why? There is a theory reals@abs_lems in the NAS PVS
Library, where your lemma is welcome. From there, you can easily import
that theory and set an auto-rewrite. Let me know if this option works for
you and add the lemma there.
Cesar A. Munoz NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx Bldg. 1220 Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446 Fax: +1 (757) 864 4234
On 7/7/15 9:35 PM, "pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on
behalf of Ben Hocking"
<pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx on behalf of
>Is there a way to “extend” prelude.pvs? For example, if I want to make
>the following proven lemma available to proofs in any theory without
>requiring them to have an IMPORTING statement for the helper lemma:
>FORALL(a: real, nnx: nnreal, b: real, nny: nnreal):
>Is there a way to do this? I’ve tried renaming the containing file
>prelude.pvs (in the current working directory), but that did not do the