[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
library path
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.