dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 02:58:26 +00:00
Code Issues Releases Wiki Activity

Compare commits

base: dhil:2cecb13d3410ef2d1d686778046ef8d8420b7483
Branches Tags
dhil:master
...
compare: dhil:72b54ad278d450c525ead83fffcd4c11523f818c
Branches Tags
dhil:master

2 Commits
2cecb13d34 ... 72b54ad278

Author SHA1 Message Date
Daniel Hillerström
72b54ad278 Add missing space in 'Evaluationcontexts' in Figure 3.5 2023-01-09 14:45:32 +00:00
Daniel Hillerström
01e707822f Fix typo in T-Let Figure 3.4 2023-01-09 14:42:09 +00:00
1 changed files with 3 additions and 3 deletions
Expand all files Collapse all files

6
thesis.tex
View File

@@ -6547,9 +6547,9 @@ Computations
% Let % Let
\inferrule*[Lab=\tylab{Let}] \inferrule*[Lab=\tylab{Let}]
{\typc{\Delta;\Gamma}{M : A}{E} \\ {\typc{\Delta;\Gamma}{M : A}{E} \\
\typ{\Delta;\Gamma, x : A}{N : C} \typc{\Delta;\Gamma, x : A}{N : B}{E}
} }
{\typ{\Delta;\Gamma}{\Let \; x \revto M\; \In \; N : C}} {\typc{\Delta;\Gamma}{\Let \; x \revto M\; \In \; N : B}{E}}
\end{mathpar} \end{mathpar}
\caption{Typing rules} \caption{Typing rules}
\label{fig:base-language-type-rules} \label{fig:base-language-type-rules}
@@ -6673,7 +6673,7 @@ that the binder $x : A$.
\EC[M] &\reducesto& \EC[N], \hfill\quad \text{if } M \reducesto N \\ \EC[M] &\reducesto& \EC[N], \hfill\quad \text{if } M \reducesto N \\
\end{reductions} \end{reductions}
\begin{syntax} \begin{syntax}
\slab{Evaluation contexts} & \mathcal{E} \in \EvalCat &::=& [~] \mid \Let \; x \revto \mathcal{E} \; \In \; N \slab{Evaluation~contexts} & \mathcal{E} \in \EvalCat &::=& [~] \mid \Let \; x \revto \mathcal{E} \; \In \; N
\end{syntax} \end{syntax}
% %
%\dhil{Describe evaluation contexts as functions: decompose and plug.} %\dhil{Describe evaluation contexts as functions: decompose and plug.}