[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Problem importing theories
I have a problem importing theories in PVS. Assume that we have a
theory T1 with non-interpreted types R and D as parameters. This theory
contains specifications of some algorithms and it has been proved
using the command "prove-importchain".
I want to instantiate this theory T1 for a given pair of interpreted
types (like strings or naturals, for example) in order to execute the
algorithms using the PVS-ground-evaluator. For example:
Typechecking (with the command typecheck) reports the following error
Error: the assertion itheory failed
I have been trying to see why this error occurs, but I have not found it
in the documentation.
Thanks in advance for your help.