[CZT-Users] Z Standard issues related to user-defined operators

[Pablo R. M. <rod...@gm...>]

Hi czt'ers,

I am having troubles in determining, from the Z Standard, which names are
valid (and which are not) for user-defined operators. In Page 28, the Z
Standard assures "Each operator template creates additional keyword-like
associations between WORDs and operator tokens.". However, not all WORD
seems to be accepted. And I could not find more restrictions about this
issue in the Z Standard.

For example, the following paragraphs are accepted:

1)

\begin{schema}{OperatorUse}
\_ <_1 \_: \nat \rel \nat \\
t,u: \nat
\where
 t <_1 u
\end{schema}

2)

\begin{zed}
 \function 40 \leftassoc (\_ \ope \_)
\end{zed}

\begin{gendef}[X]
\_ \ope \_: (\nat \cross \nat) \fun \nat
\where
\forall x,y: \nat @ x \ope y = x - y
\end{gendef}

but the following are rejected:

3)

\begin{gendef}[X]
\_ <1 \_: X \rel X
\end{gendef}

4)

\begin{schema}{OperatorUse}
\_ <? \_: \nat \rel \nat \\
t,u: \nat
\where
 t <? u
\end{schema}

5)

\begin{zed}
 \function 40 \leftassoc (\_ ope \_)
\end{zed}


I suppose that the name cannot start with a letter (case in which it must be
prefixed by a '\') nor finish with a stroke (case in which it is a
DECORDWORD instead of a WORD). However, I understand that <1 and 1< are
valid WORD's. In summary, I would like to determine a complete and more
precise set of rules.

Additionally, which situations, where an operator appear, needs to
previously define the corresponding operator template paragraph and which
not? The following two paragraphs are accepted without one of these
paragraphs:

\begin{gendef}[X]
\_ <_1 \_: X \rel X
\end{gendef}


\begin{schema}{State}
a,b: \nat
\where
a <_1 b
\end{schema}


Thanks in advance,

Pablo Rodriguez Monetti