diff options
Diffstat (limited to 'sec/systemt.ltx')
| -rw-r--r-- | sec/systemt.ltx | 28 |
1 files changed, 14 insertions, 14 deletions
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} \] |