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

*To*: pvs-help@csl.sri.com*Subject*: library path*From*: Mamoun FILALI-AMINE <filali@irit.fr>*Date*: Thu, 4 Mar 1999 15:40:56 +0100 (MET)

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 works if finite_sets is already known. But does not work otherwhise. It does not seem possible to specificy a library path in the heading of a theory? thanks.

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