summaryrefslogtreecommitdiff
path: root/test/phase5/exact-datatype-nested.tex
blob: 190176f182c78548ee0540329f2312a9a1907aae (plain)
1
2
3
4
5
6
\begin{datatype}\label{phase5_nested_data}
    Define $\phasefivenesteddata$ inductively as follows.
    \begin{enumerate}
        \item $\phasefivenested{p} \in \phasefivenesteddata$ for $p \in \pow{\phasefivenesteddata}$.
    \end{enumerate}
\end{datatype}