[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] How can I fix this?
I wrote a PVS theory as below:
x: VAR real
test: LEMMA(FORALL x: x = ((7-sqrt(37))/6) OR x = ((7+sqrt(37))/6)
When I run it, PVS displays the error
"Expecting an expression
No resolution for sqrt with arguments of possible types:
37 : reals.real"
1) I do not understand the error content. Please explain it for me.
2) How can I fix it?
Thanks a lot.