[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: library path
Dave Stringer-Calvert writes:
> > The manual explains how to declare a path for a library
> > and import something startring with this path:
> > fs: LIBRARY = "xxx/PVS/lib/finite_sets"
> > IMPORTING fs@finite_sets
> > My problem arises when I want to import a theory in the
> > heading of a theory:
> > e_r[Ix,D:TYPE, (IMPORTING finite_sets[Ix]) c:finite_set[Ix]]: THEORY
> > BEGIN
> > ...
> > END e_r
> It is not possible to get this behavior from PVS 2.2 - it is a deficiency
> in the language. We will modify the language to allow this in PVS 2.3.
Perhaps this would be a good place to use PVS's other library
mechanism. If you type M-x load-prelude-library and enter
"xxx/PVS/lib/finite_sets/" in response to the prompt, the working
context will (in essence) extend the prelude with all the theories in
the finite_sets context. Then you would be able to pass a finite set
as a theory parameter.
-- Paul S. Miner | phone: (757) 864-6201
-- 1 South Wright St. / MS 130 | fax: (757) 864-4234
-- NASA Langley Research Center | mailto:firstname.lastname@example.org
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/