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

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


When I try to define an inductive type like below:

   ivlOP :  DATATYPE
        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.