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

[PVS-Help] How can I fix this?

Hello everybody,


I wrote a PVS theory as below:

test:  THEORY
BEGIN
x: VAR real
test: LEMMA(FORALL x: x = ((7-sqrt(37))/6) OR x = ((7+sqrt(37))/6)
IMPLIES x>=0)
END test

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.

Nguyen,