Synthesize self for tvars

hazelgrove · May 20, 2021 · 4410cd5 · 4410cd5
1 parent 99db512
commit 4410cd5
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/9-type-aliases-redux/latex/kind-judgements.pdf b/9-type-aliases-redux/latex/kind-judgements.pdf
diff --git a/9-type-aliases-redux/latex/kind-judgements.tex b/9-type-aliases-redux/latex/kind-judgements.tex
@@ -186,7 +186,7 @@
 		\inferrule[KSVar]{
 			t : \hkappa \in \hPhi
 		} {
-			\kindSyn{\Delta;\hPhi}{t}{\hkappa}
+			\kindSyn{\Delta;\hPhi}{t}{\KSing{t}}
 		}
 		\and
 		\inferrule[KSUVar]{
@@ -338,7 +338,7 @@
 		\inferrule[TElabSVar]{
 			t : \hkappa \in \hPhi
 		} {
-			\elabSyn{\hPhi}{t}{\hkappa}{t}{\EmptyDelta}
+			\elabSyn{\hPhi}{t}{\KSing{t}}{t}{\EmptyDelta}
 		}
 		\and
 		\inferrule[TElabSUVar]{