Mercurial > urweb
changeset 573:33500a15b872
More manual bug reports from megacz
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Wed, 24 Dec 2008 10:48:31 -0500 |
| parents | 57018f21cd5c |
| children | 813f1e78d9d0 |
| files | doc/manual.tex |
| diffstat | 1 files changed, 6 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/doc/manual.tex Sun Dec 21 12:30:57 2008 -0500 +++ b/doc/manual.tex Wed Dec 24 10:48:31 2008 -0500 @@ -435,11 +435,11 @@ $$\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 @@ \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 @@ & \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