test/examples/inductive.tex


1
2
3
4
5
6
7
8

% Direct bounded inductive example checked through the typed fixed-point path.

\begin{inductive}\label{fin}
    Define $\fin{A}\subseteq\cumul{A}$ inductively as follows.
    \begin{enumerate}
        \item $A\in\fin{A}$.
    \end{enumerate}
\end{inductive}