summaryrefslogtreecommitdiff
path: root/sec/encoding.ltx
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2025-06-19 00:26:46 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2025-06-19 00:26:46 +0100
commit437b0c42e713774e7a27ccdc1f08770e30aeacbd (patch)
tree1800fab6ef4618b3fa3ef6f116fc03d43a968b76 /sec/encoding.ltx
parentf99a6ff28455e693865ed7174a334f0c68b46135 (diff)
Fix missing character warning.
Diffstat (limited to 'sec/encoding.ltx')
-rw-r--r--sec/encoding.ltx2
1 files changed, 1 insertions, 1 deletions
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