%
% test2.in
% Copyright (C) J.M. Spivey 1989
%

\begin{zed}
\t0	\forall DISK\_POOL: \nat @
\t1		"DISK\_POOL" = 0
\end{zed}

\begin{zed} (3 + 4 = 5) \end{zed}
\begin{zed} 3 (+ 4 = 5) \end{zed}
\begin{zed} 3 + (4 = 5) \end{zed}
\begin{zed} 3 + 4 (= 5) \end{zed}
\begin{zed} 3 + 4 = (5) \end{zed}
\begin{zed} (\_+\_)(3, 4) = 5 \end{zed}
\begin{zed} (-) ((3) + 4) = 5 \end{zed}

\begin{zed}
	x : \nat
\end{axdef}

\begin{axdef}
	gulp: \power \nat
\end{zed}

\begin{zed}
	2 + 2 = \\
	\forall x: \nat @ x+1 > x
\end{zed}

Quantifier syntax:

\begin{zed}
	\forall x: \nat @ x > 1 \implies
		\exists y: \nat @ x < y < 2 * x
\end{zed}

A bad set expression:

\begin{zed}
	\empty = \{ foo, 2+2, x: \nat \}
\end{zed}

Bad decoration in schema def:

\begin{zed}
	SEP1a' \defs [ x: \nat ]
\end{zed}

\begin{schema}{SEP1b''}
	x: \nat
\end{schema}

\begin{zed}
	2 + 2 = 4
% \end{zed}
