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

\documentstyle[12pt,fuzz]{article}
\begin{document}

%% New language features added in V2

%% Let predicates and expressions

\begin{zed}
  foo == (\LET x == 3 @ (\LET y == x @ x+y))
\also
  baz == (\LET (\_ + \_) == (\lambda x, y: \nat @ \{x, y\}) @ foo + foo)
\also
  \LET pop == foo @ foo = pop
\end{zed}

%% Renaming a la mode
\begin{schema}{A} x, y: \nat \end{schema}

\begin{zed}
  R == \{~A; A[z/x] | z = x~\}
\end{zed}

\begin{schema}{B} A; A[z/x] \end{schema}

%% Underlined infixes
\begin{zed}
  \exists R: \num \rel \num @ \forall x, y: \num @ x \inrel{R} y
\end{zed}

\begin{zed}
  asdf == 0 + (\IF 1 = 2 \THEN 3 \ELSE 4)
\end{zed}

\begin{schema}{State}
  x, y: \nat
\end{schema}

\begin{schema}{FetchX}
  \Delta State\\
  val!: \nat
\where
  val! = x' = x
\end{schema}

\begin{schema}{IncY}
  \Delta State\\
  val?: \nat
\where
  y' = y + val?
\end{schema}

\begin{zed} Add \defs FetchX \pipe IncY \end{zed}

\begin{zed}
  a == \emptyset[\num \cross \num] \oplus \emptyset\\
  b == \{ 1, 3, 5 \} \extract \langle 3, 1, 4, 1, 5, 9, 3 \rangle\\
\also
  squash~\{1 \mapsto 2, 3 \mapsto 4\} = \langle 2, 4 \rangle
\also
  \forall R: \{ (\_\prefix\_), (\_\suffix\_), (\_\inseq\_)\} @
    \langle \rangle \inrel{R} \langle 54 \rangle
\also
  \forall x: \bag (\bag \nat) @ 
    count~x~\lbag3\rbag = x \bcount \lbag3\rbag
\also
  \lbag 1, 2, 3 \rbag \subbageq 4 \otimes \lbag 2, 3 \rbag
\also
  \lbag 1, 2, 3 \rbag \uminus \lbag 2 \rbag = \lbag 1, 3 \rbag
\also
  2 \inbag \lbag 1, 2 \rbag
\end{zed}

\begin{schema}{Set}[X]
  val: \power X
\end{schema}

\begin{schema}{Insert}[X]
  \Delta Set[X]\\
  in?: X
\where
  val' = val \cup \{in?\}
\end{schema}

\begin{zed}
  q == \{\{1\} \mapsto \empty\} \cup (\id \_)
\end{zed}

\begin{zed}
  \lbag 1, 2, 3 \rbag \uminus \lbag 2 \rbag = \lbag 1, 3 \rbag
\also
  2 \inbag \lbag 1, 2 \rbag
\end{zed}

\end{document}
