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

Re: 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


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.

Dave

---
Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com