summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMatthew Dempsky <matthew@dempsky.org>2020-02-04 16:48:57 -0800
committerMatthew Dempsky <matthew@dempsky.org>2020-02-04 16:59:07 -0800
commit5ed96ea023de0570061660363ee55c3f9cffda18 (patch)
tree24f36ba4a06ab465c185e93ac38959d663944cd0
parent50dc9b9fe270e3d92955d71a1c027b076d719aca (diff)
Remove superfluous lambdas before guarded types
Guarded expression abstractions (fn [c ~ c] => e) begin with a lambda, but guarded types ([c ~ c] => t) do not.
-rw-r--r--doc/manual.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 8ea78e4f..b1ac0041 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -797,7 +797,7 @@ $$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \times \kappa_n)
\Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n)
}$$
-$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow \tau :: \mt{Type}}{
+$$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow \tau :: \mt{Type}}{
\Gamma \vdash c_1 :: \{\kappa\}
& \Gamma \vdash c_2 :: \{\kappa'\}
& \Gamma, c_1 \sim c_2 \vdash \tau :: \mt{Type}
@@ -963,7 +963,7 @@ $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \
& \Gamma_i \vdash e_i : \tau
}$$
-$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : \lambda [c_1 \sim c_2] \Rightarrow \tau}{
+$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : [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