Re: library path

["Paul S. Miner" <p.s.miner@larc.nasa.gov>]

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.

Regards,

-- 
-- Paul S. Miner                | phone: (757) 864-6201
-- 1 South Wright St. / MS 130  | fax:   (757) 864-4234
-- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/

---

• References:
  • library path
    • From: Mamoun FILALI-AMINE <filali@irit.fr>
  • Re: library path
    • From: Dave Stringer-Calvert <dave_sc@csl.sri.com>

• Prev by Date: Re: library path
• Next by Date: Subtyping
• Prev by thread: Re: library path
• Next by thread: PVS dump files
• Index(es):
  • Date
  • Thread