diff options
Diffstat (limited to 'sec/encoding.ltx')
| -rw-r--r-- | sec/encoding.ltx | 2 |
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 |