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

Re: library path

To: Mamoun FILALI-AMINE <filali@irit.fr>
Subject: Re: library path
From: Dave Stringer-Calvert <dave_sc@csl.sri.com>
Date: Fri, 19 Mar 1999 11:21:32 -0800
cc: pvs-help@csl.sri.com
In-reply-to: Your message of "Thu, 04 Mar 1999 15:40:56 +0100." <199903041440.PAA09253@blaise.irit.fr>


> 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

Prev by Date: library path
Next by Date: Re: library path
Prev by thread: library path
Next by thread: Re: library path
Index(es):
- Date
- Thread