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

Re: Defining new infix operators


> How can I define my own infix operators?

I'm afraid you can't do it in the current version of PVS.

It doesn't look too hard to add this capability, so we'll think about
it for the next release.

The LaTeXprinter can be used to change the way operators appear in
typeset documents.