\documentclass[../../main.tex]{subfiles}
\begin{document}
\subsubsection{Array?}
The operation $array?$ will return a boolean which indicates if the passed in argument is a Collection
\begin{schema}{Array?[V]}
  coll? : V \\
  bol! : Boolean \\
  array?~\_ : V \fun Boolean
  \where
  bol! = array?(coll?) @ bol! = true \iff coll? : Collection \implies V \hide (Scalar, KV)
\end{schema}
where $V \hide (Scalar, KV)$ is used to indicate that $coll?$ is of type $V$
\begin{zed}
  V ::= Scalar ~| ~Collection ~| ~KV
\end{zed}
but in order for $bol! = true$, $coll?$ must not be of type $Scalar ~\lor KV$ such that
\begin{argue}
  X = \langle x_{0}, x_{1}, x_{2}, x_{3}, x_{4} \rangle \\
  \t1 x_{0} = 0 \\
  \t1 x_{1} = foo \\
  \t1 x_{2} = \langle baz, \ qux \rangle \\
  \t1 x_{3} = \ldata abc \mapsto 123, \ def \mapsto 456 \rdata \\
  \t1 x_{4} = \langle \ldata ghi \mapsto 789, \ jkl \mapsto 101112 \rdata, \ \ldata ghi \mapsto 131415, \ jkl \mapsto 161718 \rdata \rangle \\
  array?(X) = true & collection by definition\\
  array?(x_{2}) = true & collection of $0 \mapsto baz$, $1 \mapsto qux$\\
  array?(x_{4}) = true & collection of maps\\
  array?(x_{0}) = false & Scalar \\
  array?(x_{1}) = false & String \\
  array?(x_{3}) = false & Map
\end{argue}
\end{document}
