Change syntax of `\judgement`

2 files changed, 17 insertions, 15 deletions

diff --git a/main.tex b/main.tex
index 1f8e1e5..17bbbee 100644
--- a/main.tex
+++ b/main.tex
@@ -162,7 +162,9 @@
 \newcommand\rangeover[2]{\overrightarrow{#1}}
 
 % Judgements for typing and such
-\newcommand\judgement[4][]{{#2} \vdash^{#1} {#3} : {#4}}
+\NewDocumentCommand\judgement{momO{:}m}{%
+  {#1} \vdash^{\IfNoValueF{#2}{#2}} {#3} \mathrel{#4} {#5}
+}
 \newcommand\jdgmnt[3]{{#2} \vdash {#3}~\mathrm{#1}}
 
 % List operators
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}
   \]