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

[PVS-Help] semantic attachment problem


I am quite new in pvs. I have a pvs file which contains a theory. Then in pvs-attachment I wrote a defattach for one of the theories. I can see the result in ground evaluator. But In addition to the result , it gives me this message : Result not ground.  Cannot convert back to PVS.
The other problem is that how I can get the value of the defattach in my pvs file or at least in another lisp file that loads my pvs file !?

Thank you