Re: [CZT-Users] Custom LaTeX commands

[James W. <jw...@cs...>]

Hi again,

Further to my last e-mail, I was able to define mult in the way suggested by Tim Miller. However, I'm getting a type-check error that I don't understand:

%I define my generic:
%%Zpreword \mult mult
\begin{zed}
	\generic (\mult~\_)
\end{zed}

% This is used in the gendef
\begin{zed}
MultTy ::= mm | mo | om | mzo | zom | oo | zozo | zoo | ozo | ms | sm
| ss \\ \t1
| so | os | szo | zos
\end{zed}

% I define mult mathematically
\begin{gendef}[X, Y]
  \mult\_: \power  ((X \rel  Y) \cross  \power  X \cross  \power  Y \cross  MultTy \cross  \finset  \nat  \cross  \finset  \nat )
\where
\forall  r: X \rel  Y; sx: \power  X; sy: \power  Y; s_1, s_2: \finset
\nat  @ \\ \t1
     (\mult (r, sx, sy, mm, s_1, s_2)) \iff  r \in sx \rel  sy
\also
	...
\end{gendef}

But I get the following error:

Schema expression required in expression predicate
	Expression: ( mult ( r , sx , sy , mm , s_{1}~, s_{2} ) )
	Type: \power ( \power ( X \cross Y ) \cross \power X \cross \power Y \cross MultTy \cross \power \arithmos \cross \power \arithmos )
Name "mult~\_" requires no parameters within its own definition

Have I defined mult incorrectly? This isn't my own Z, and has been used in the past (but not on ISO Z). I'm just trying to get it to type-check. (For those interested in what mult is meant to do - it's defining multiplicities between classes - mm=many to many, mo=many to one, and so on)

One other thing, related to latex definitions. I do the following:

\newcommand{\oset}{\mathcal{O}}
%%Zword \oset

\begin{schema}{Example}
	\oset : \num
\end{schema}

But I get a "Syntax error at symbol COLON" parse exception. How should I define \oset if I want to use it as a declaration name? I've been looking through the Z standard, but can't work it out.

Thanks again, your help is really appreciated.

James