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

[PVS-Help] outfix operators



How can I use outfix operators?  The following theory causes 

"Error: Unrecognized expr -"

to be output in buffer *Error Output*, and gives me the choice:

SPC-scroll, I-ignore, K-keep, A-abort sends and keep or B-break:

The theory is:

test_thy: THEORY
BEGIN

	{||}: [int -> int] = (lambda (n: int): n+n)

	six: int = {| 3 |}
	six2: int = {| 3 |}


END test_thy

Using {||} as a prefix operator appears to work fine

Thanks,
Rob