summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-12-24 10:48:31 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-12-24 10:48:31 -0500
commit9030684acadec34adb8f08547dffe250ff4449d6 (patch)
tree870b77ae0aa4a7de596bfb6be5d62412f7aa042e
parentd5c3faacb1c3114fe6802973a62528cda8be8ac7 (diff)
More manual bug reports from megacz
-rw-r--r--doc/manual.tex11
1 files changed, 6 insertions, 5 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index af905574..0e756426 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -435,11 +435,11 @@ $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
$$\infer{\Gamma \vdash \mt{fold} :: ((\mt{Name} \to \kappa_1 \to \kappa_2 \to \kappa_2) \to \kappa_2 \to \{\kappa_1\} \to \kappa_2}{}$$
-$$\infer{\Gamma \vdash (\overline c) :: (k_1 \times \ldots \times k_n)}{
- \forall i: \Gamma \vdash c_i :: k_i
+$$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \times \kappa_n)}{
+ \forall i: \Gamma \vdash c_i :: \kappa_i
}
-\quad \infer{\Gamma \vdash c.i :: k_i}{
- \Gamma \vdash c :: (k_1 \times \ldots \times k_n)
+\quad \infer{\Gamma \vdash c.i :: \kappa_i}{
+ \Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n)
}$$
$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{
@@ -584,6 +584,7 @@ $$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
\quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
\Gamma \vdash e_1 : \$c_1
& \Gamma \vdash e_2 : \$c_2
+ & \Gamma \vdash c_1 \sim c_2
}$$
$$\infer{\Gamma \vdash e \rcut c : \$c'}{
@@ -609,7 +610,7 @@ $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \
& \Gamma_i \vdash e_i : \tau
}$$
-$$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow e : [c_1 \sim c_2] \Rightarrow \tau}{
+$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : \lambda [c_1 \sim c_2] \Rightarrow \tau}{
\Gamma \vdash c_1 :: \{\kappa\}
& \Gamma \vdash c_2 :: \{\kappa\}
& \Gamma, c_1 \sim c_2 \vdash e : \tau