Re: [PVS-Help] importing another theory

[Sam Owre <owre@xxxxxxxxxxx>]

Hi,

Could you send me your PVS files?  "No next method" indicates a bug in
PVS, for which there is not a simple fix - it depends on the methods
involved.

Thanks,
Sam

sujith cs <cs_sujith@yahoo.com> wrote:

> Sir,
> 
>    I am converting a program written in c language to typed transition system
> accepted by pvs theorem prover.a main program calls another procedure.
> 
> For eg.
> 
> Procedure rt(int x, int y)
> 
> ……..
> 
> …..
> 
> X=dt(a,b)
> 
> .
> 
> I want to express this .
> 
> I wrote two theories named rt and dt. when I tried to import dt in rt, an error
> message came “there is no next method for method” what is it.how to resolve it.