From 0fad2cde9763828c16a4aa59e8335e668c8e964f Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 25 Jun 2025 17:49:22 +0100 Subject: Rename labels to be more consistent. --- sec/lang.ltx | 8 ++++---- 1 file 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 -- cgit v1.2.3