[PVS-Help] the problem "No methods applicable for generic function"

[Zheng Bingzhou <bingzhou.zheng@xxxxxxxxx>]

Hi,

When I try to define an inductive type like below:

   ivlOP :  DATATYPE
   BEGIN
        id : id?
        add (lop, rop: ivlOP): add?
        sub (lop, rop: ivlOP): sub?
        mul (lop, rop: ivlOP): mul?

        div  (lop, rop: ivlOP): div?
   END ivlop

I do the type-checking and get the error "No methods applicable for generic function". 

I just begin to use PVS, and write this datatype based on a tutorial. I wonder what's wrong with this definition? any advice

By the way, I use PVS5.0 with the library nasalib.

Thanks,
Bingzhou