From 0fad2cde9763828c16a4aa59e8335e668c8e964f Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
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(-)

(limited to 'sec/lang.ltx')

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

