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

[PVS-Help] I cant typecheck theory



When I import the library reals@polinomials of NASA Larc:
http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html 

and try to typecheck my theory it gives the following error message:
Theory temp not typechecked?
and prompts for scroll, ignore, keep, abort or break

I'm using the next theory for replicate the error

temp : THEORY

  BEGIN

  importing reals@polynomials

    a, b, d: VAR sequence[real]

  END temp

Any idea? 

Thanks in advance