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

[PVS-Help] Re: the problem "No methods applicable for genericfunction"



[4c] pvs(41): :bt
Evaluation stack:

(method no-applicable-method (t)) <-
  let <- let <- let* <- let* <- let* <- :unknown <-
  update-parsed-file <- parse-file* <- (method parse-file (string)) <-
  typecheck-file <- let <- throw <- let* <- let <- catch <- eval <-
  cerror <- (method no-applicable-method (t)) <- let <- let <- let* <-
  let* <- let* <- :unknown <- update-parsed-file <- parse-file* <-
  (method parse-file (string)) <- typecheck-file <- letthrow <-  ...

2012/1/24 Zheng Bingzhou <bingzhou.zheng@gmail.com>
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