From 85905c93f74238b056f4b0ee0864782947ae02a6 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 12 Jun 2025 14:36:30 +0100
Subject: Change syntax of `\judgement`

---
 sec/systemt.ltx | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index d25bd22..63cd7a7 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -9,7 +9,7 @@ System~T is a simply-typed lambda calculus. The types are naturals
 application operators, we have \zero{} and \suc{} for zero and
 successor, as well as \primreckw{}, the primitive
 recursor. \Cref{fig:syst-typing} shows the typing judgements, where
-\(\judgement[T]{\Gamma}{t}{A}\) means that \(t\) is System~T term of type
+\(\judgement{\Gamma}[T]{t}{A}\) means that \(t\) is System~T term of type
 \(A\) in context \(\Gamma\), and \cref{fig:syst-eq} the equational theory.
 
 \begin{figure}
@@ -17,34 +17,34 @@ recursor. \Cref{fig:syst-typing} shows the typing judgements, where
   \begin{array}{ccc}
     \begin{prooftree}
       \hypo{x : A \in \Gamma}
-      \infer1{\judgement[T]{\Gamma}{x}{A}}
+      \infer1{\judgement{\Gamma}[T]{x}{A}}
     \end{prooftree}
     &
     \begin{prooftree}
-      \hypo{\judgement[T]{\Gamma, x : A}{t}{B}}
-      \infer1{\judgement[T]{\Gamma}{\lambda x. t}{A \to B}}
+      \hypo{\judgement{\Gamma, x : A}[T]{t}{B}}
+      \infer1{\judgement{\Gamma}[T]{\lambda x. t}{A \to B}}
     \end{prooftree}
     &
     \begin{prooftree}
-      \hypo{\judgement[T]{\Gamma}{f}{A \to B}}
-      \hypo{\judgement[T]{\Gamma}{t}{A}}
-      \infer2{\judgement[T]{\Gamma}{f~t}{B}}
+      \hypo{\judgement{\Gamma}[T]{f}{A \to B}}
+      \hypo{\judgement{\Gamma}[T]{t}{A}}
+      \infer2{\judgement{\Gamma}[T]{f~t}{B}}
     \end{prooftree}
     \\\\
     \begin{prooftree}
-      \infer0{\judgement[T]{\Gamma}{\zero}{\nat}}
+      \infer0{\judgement{\Gamma}[T]{\zero}{\nat}}
     \end{prooftree}
     &
     \begin{prooftree}
-      \hypo{\judgement[T]{\Gamma}{t}{\nat}}
-      \infer1{\judgement[T]{\Gamma}{\suc~t}{\nat}}
+      \hypo{\judgement{\Gamma}[T]{t}{\nat}}
+      \infer1{\judgement{\Gamma}[T]{\suc~t}{\nat}}
     \end{prooftree}
     &
     \begin{prooftree}
-      \hypo{\judgement[T]{\Gamma}{t}{\nat}}
-      \hypo{\judgement[T]{\Gamma}{u}{A}}
-      \hypo{\judgement[T]{\Gamma, x : A}{v}{A}}
-      \infer3{\judgement[T]{\Gamma}{\primrec{t}{u}{(x.v)}}{A}}
+      \hypo{\judgement{\Gamma}[T]{t}{\nat}}
+      \hypo{\judgement{\Gamma}[T]{u}{A}}
+      \hypo{\judgement{\Gamma, x : A}[T]{v}{A}}
+      \infer3{\judgement{\Gamma}[T]{\primrec{t}{u}{(x.v)}}{A}}
     \end{prooftree}
   \end{array}
   \]
-- 
cgit v1.2.3

