diff options
| -rw-r--r-- | main.tex | 11 | ||||
| -rw-r--r-- | sec/compiler.ltx | 12 | ||||
| -rw-r--r-- | sec/encoding.ltx | 2 | ||||
| -rw-r--r-- | sec/intro.ltx | 2 | ||||
| -rw-r--r-- | sec/lang.ltx | 2 |
5 files changed, 14 insertions, 15 deletions
@@ -24,16 +24,13 @@ \usepackage[ datamodel=acmdatamodel, - style=acmnumeric, - giveninits, - doi, - eprint = false + style=acmnumeric ]{biblatex} %% bibliography configuration \usepackage{booktabs} %% table formatting \usepackage{ebproof} %% proof trees \usepackage{expl3} %% Latex 3 \usepackage{enumitem} %% format contributions list -\usepackage{float} %% forcing appendix figures +\usepackage{float} %% forcing figures \usepackage{hyperref} %% hyperlinks within document \usepackage{mathtools} %% matrix alignment \usepackage[verbatim]{minted} %% code formatting @@ -336,6 +333,7 @@ \ExplSyntaxOff %%% Substitution + \ExplSyntaxOn \NewDocumentCommand \squid_subpart:nn {m m} {{#1} \mapsto {#2}} \NewDocumentCommand \squid_contsub:n {> {\SplitArgument{1}{/}} m} @@ -351,7 +349,8 @@ { {#1} [ \squid_checksub [] #2 } \ExplSyntaxOff -\newcommand\submult[2]{{#1}[ {#2} ]} + +\NewDocumentCommand\suball{mm}{{#1} [#2]} %% Document %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/sec/compiler.ltx b/sec/compiler.ltx index cd600ac..3a3cebc 100644 --- a/sec/compiler.ltx +++ b/sec/compiler.ltx @@ -174,12 +174,12 @@ prior computations, so we do not need to reference the raw AST. \Cref{fig:bidir} shows how we have modified the \lang{} typing rules for bidirectional type checking. The changes are standard~\cref{bidir}. Products can both check and synthesise types. -The \rollkw{} operator can only be checked as there is no unique -correct guess for the shape type. The body of a \foldkw{} must be -checked. The induction hypothesis is added to the context, so its type -must be known before processing the body. As the induction hypothesis -is filled by the motive, the only mode-correct way to obtain the -motive type is for \foldkw{} to be checked. +The \roll{} operator can only be checked as there is no unique correct +guess for the shape type. The body of a \foldkw{} must be checked. The +induction hypothesis is added to the context, so its type must be +known before processing the body. As the induction hypothesis is +filled by the motive, the only mode-correct way to obtain the motive +type is for \foldkw{} to be checked. The Idris~2 type for certifying the bidirectional judgement is almost a direct translation of the judgement in \cref{fig:bidir}. The diff --git a/sec/encoding.ltx b/sec/encoding.ltx index e88a628..0c58aea 100644 --- a/sec/encoding.ltx +++ b/sec/encoding.ltx @@ -118,7 +118,7 @@ Given a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), a type variable \(X \in \Psi\), a type environment \(\alpha\) and a type \(S\), we define a term \(\mathsf{distrib}\) of type \[ -\submult{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \submult{A}{\alpha} +\suball{A}{\sub{\alpha}{X/S \to S \times \alpha(X)}} \to S \to S \times \suball{A}{\alpha} \] that calls each accumulator within \(A\) in sequence. The definition is by induction on the well-formedness derivation of \(A\). The diff --git a/sec/intro.ltx b/sec/intro.ltx index 0a50ff4..f520bc4 100644 --- a/sec/intro.ltx +++ b/sec/intro.ltx @@ -24,7 +24,7 @@ \subsubsection*{Contributions}% In this paper we: -\begin{itemize} +\begin{itemize}[nosep] \item contrast different methods for encoding inductive types in System~T (\cref{M-subsec:encoding-strategies}); \item give the syntax, typing rules and equational theory for diff --git a/sec/lang.ltx b/sec/lang.ltx index e675a85..1319d5e 100644 --- a/sec/lang.ltx +++ b/sec/lang.ltx @@ -58,7 +58,7 @@ unrepresentable in some models of System~T}. For any type \(A\) such that \(\jdgmnt{ty}{\Psi}{A}\) and a substitution from variables \(X \in \Psi\) to types \(\jdgmnt{ty}{\Theta}{f(X)}\), we have - \(\jdgmnt{ty}{\Theta}{\submult{A}{f}}\). + \(\jdgmnt{ty}{\Theta}{\suball{A}{f}}\). \end{proposition} \begin{figure} |