diff options
| -rw-r--r-- | sec/lang.ltx | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/sec/lang.ltx b/sec/lang.ltx index c94f388..af652a1 100644 --- a/sec/lang.ltx +++ b/sec/lang.ltx @@ -32,11 +32,11 @@ \infer1{\jdgmnt{ty}{\Psi}{\mu X. A}} \end{prooftree} \] - \caption{Well-formedness of \lang{} types}\label{fig:artist-wf} + \caption{Well-formedness of \lang{} types}\label{fig:lang-wf} \end{figure} In this section we introduce \lang{}, a simply-typed lambda calculus -with \emph{regular types}. \Cref{fig:artist-wf} shows the +with \emph{regular types}. \Cref{fig:lang-wf} shows the well-formedness judgement for types, where \(\jdgmnt{ty}{\Psi}{A}\) means that \(A\) is a type using variables from \(\Psi\). We have labelled \(n\)-ary products and sums, where the set of labels is finite. Types @@ -124,10 +124,10 @@ claim the type unrepresentable in some models of System~T}. } \end{array} \] - \caption{Typing judgements for \lang{}}\label{fig:artist-types} + \caption{Typing judgements for \lang{}}\label{fig:lang-ty} \end{figure} -\Cref{fig:artist-types} gives the typing judgements for \lang{}. The +\Cref{fig:lang-ty} gives the typing judgements for \lang{}. The introduction and elimination rules for functions, products and sums are standard, as are the rules for variables and let bindings. The two new operators, \roll{} and \foldkw{}, introduce values of an inductive |