summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Matthew Dempsky <matthew@dempsky.org>2020-02-04 16:44:59 -0800
committerGravatar Matthew Dempsky <matthew@dempsky.org>2020-02-04 16:50:44 -0800
commit77d355444228fcde64572b86920e87df139fa4ed (patch)
tree661676a16138f8c359ec2d1cd551fdf84f2ef68c
parentdbdf458dc49191a6f355a16bae839a2d618513b7 (diff)
Fix record type shorthand
The syntax is {c : c}, not {c = c}. Also, replace uses of shorthand (both correct and incorrect) in semantics rules with elaborated $[c = c].
-rw-r--r--doc/manual.tex6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index bf844a0c..253cdc5d 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -622,7 +622,7 @@ There are a variety of derived syntactic forms that elaborate into the core synt
In many contexts where record fields are expected, like in a projection $e.c$, a constant field may be written as simply $X$, rather than $\#X$.
-A record type may be written $\{(c = c,)^*\}$, which elaborates to $\$[(c = c,)^*]$.
+A record type may be written $\{(c : c,)^*\}$, which elaborates to $\$[(c = c,)^*]$.
The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
@@ -933,7 +933,7 @@ $$\infer{\Gamma \vdash e [\kappa] : [X \mapsto \kappa]\tau}{
\Gamma, X \vdash e : \tau
}$$
-$$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
+$$\infer{\Gamma \vdash \{\overline{c = e}\} : \$[\overline{c = \tau}]}{
\forall i: \Gamma \vdash c_i :: \mt{Name}
& \Gamma \vdash e_i : \tau_i
& \forall i \neq j: \Gamma \vdash c_i \sim c_j
@@ -1000,7 +1000,7 @@ $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i
& \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
}$$
-$$\infer{\Gamma \vdash \{\overline{X = p}\} \leadsto \Gamma_n; \{\overline{X = \tau}\}}{
+$$\infer{\Gamma \vdash \{\overline{X = p}\} \leadsto \Gamma_n; \$[\overline{X = \tau}]}{
\Gamma_0 = \Gamma
& \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
}