[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Error: No Method Applicable for Generic Function
I tried your approach and I still got the same error
Then I tried something. Recall originally I had,
theory2 is located in foo
which means that in theory1, theory3 should be imported. At this point I still
had the error. Then just for the sake of experimenting I modified theory1 as
theory2 still imports theory3 and now theory1 imports both theory2 and
theory3. Somehow PVS was able to typecheck the modified theory1.
Why should I import theory3 in theory1 when it is already imported in theory2?
On Wednesday 08 March 2006 04:04 pm, you wrote:
> IMHO this is a better approach:
> 1. Define the environment variable PVS_LIBRARY_PATH:
> where <fooroot> is the full path to the root of foo, i.e.,
> $ test -d <fooroot>/foo && echo Yes
> should print Yes.
> 2. Remove lib:LIBRARY = "foo/" from theory1 and import theory2 as
> IMPORTING foo@theory2
> 3. Done.
You never hesitate to tackle the most difficult problems.