Re: [CZT-Devel] (implicit) operator templates in (Delta) schemas - ???

[Tim M. <tm...@un...>]

Hi Leo,

You wrote:
> \begin{schema}{Op}
>     \Delta~S
> \where
>      (\_ R \_)' = .....
> \end{schema}
>
> the dashed name is clearly undeclared. Yet, in ZEves, the "dashed" name gets declared
> as an Operator. What the standard says about such "implicit" op temp declarations?
>
There dashed name is declared, but it must be referenced as (\_~ {R}' 
\_). The following example parses and typechecks using CZT:

%%Zinword \R R

\begin{zed}
  \relation (\_ \R \_)
\end{zed}

\begin{schema}{S}
      \_ \R \_ : \nat \rel \nat
\end{schema}

\begin{axdef}
    S~'
\where
     (\_~ {\R}' \_) = \{(1,1)\}
\end{axdef}

\begin{axdef}
\where
   1~ {\R}' 1
\end{axdef}

So here, the name {\R}' is not implicitly declared as a operator, but it 
can be used as one because \R is declared as an operator.

According to the standard, the expression (\_ R \_)' should parse as 
schema decoration, so is not accepted by the CZT typechecker.

Cheers,
Tim