From 5ed96ea023de0570061660363ee55c3f9cffda18 Mon Sep 17 00:00:00 2001 From: Matthew Dempsky Date: Tue, 4 Feb 2020 16:48:57 -0800 Subject: 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. --- doc/manual.tex | 4 ++-- 1 file 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 -- cgit v1.2.3