summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Matthew Dempsky <matthew@dempsky.org>2020-02-04 16:46:20 -0800
committerGravatar Matthew Dempsky <matthew@dempsky.org>2020-02-04 16:53:52 -0800
commit50dc9b9fe270e3d92955d71a1c027b076d719aca (patch)
tree467fec5096f1eefd931213bd936fb0f0f1c4230f
parent77d355444228fcde64572b86920e87df139fa4ed (diff)
Fix typos in kinding judgments
Kind-polymorphism is written as "X --> k", not "X -> k".
-rw-r--r--doc/manual.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 253cdc5d..8ea78e4f 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -767,10 +767,10 @@ $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
}$$
$$\infer{\Gamma \vdash c[\kappa'] :: [X \mapsto \kappa']\kappa}{
- \Gamma \vdash c :: X \to \kappa
+ \Gamma \vdash c :: X \longrightarrow \kappa
& \Gamma \vdash \kappa'
}
-\quad \infer{\Gamma \vdash X \Longrightarrow c :: X \to \kappa}{
+\quad \infer{\Gamma \vdash X \Longrightarrow c :: X \longrightarrow \kappa}{
\Gamma, X \vdash c :: \kappa
}$$