diff options
Diffstat (limited to 'rules/rules.tex')
| -rw-r--r-- | rules/rules.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/rules/rules.tex b/rules/rules.tex index ee1d54b..763870e 100644 --- a/rules/rules.tex +++ b/rules/rules.tex @@ -191,7 +191,7 @@ \renewcommand\Dd[3]{D^2_{#1,#2,#3}}% \newcommand\Dac{D_{2\mathrm{Ac}}}% \begin{gather*} - \DD{\Gamma_M}{\Gamma_A}\,t = (\Dzero\Gamma\,t, \Dsave\Gamma\,t, \Dp\Gamma\,t, \Dmerge{\Gamma_M}\,t, \Dd{\Gamma_M}{\Gamma_A}{d}\,t) \qquad(\Gamma \coloneqq \Gamma_M \cup \Gamma_A) \\ + \DD{\Gamma_M}{\Gamma_A}\,t = (\Dzero\Gamma\,t, \Dsave\Gamma\,t, \Dp\Gamma\,t, \Dmerge{\Gamma_M}\,t, \Dd{\Gamma_M}{\Gamma_A}{d}\,t) \qquad(\Gamma \coloneqq \Gamma_M \cup \Gamma_A\text{, disjoint}) \\ \Dac[x_1 : \tau_1, \ldots, x_n : \tau_n] \coloneqq x_1 : \mathrm{Accum}\ \tau_1, \ldots, x_n : \mathrm{Accum}\ \tau_n \\ \Gamma \vdash t : \tau \;\;\leadsto\;\; @@ -214,7 +214,7 @@ Accumulation effect: \frac{\tau_1 \overset{p}{\rightsquigarrow} \tau_2, \tau_{\mathrm{idx}} \quad \Gamma \vdash t_1 : \tau_{\mathrm{idx}} \quad \Gamma \vdash t_2 : D_2\,\tau_2 - \quad \Gamma \vdash t_2 : \mathrm{Accum}\ \tau_1} + \quad \Gamma \vdash t_3 : \mathrm{Accum}\ \tau_1} {\Gamma \vdash \underline{\mathrm{accum}}_p\ t_1\ t_2\ t_3 : \tUnit} \end{gather*} |