core-spec: Fix S_MatchData

Previously, it would substitute e for n without an e being around. I clarify that by naming the scrutinee e.
ayberkt · Dec 2, 2016 · 90c5af4 · 90c5af4
1 parent eb6f673
commit 90c5af4
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
@@ -66,9 +66,10 @@ S |- e --> e'
 S |- case e as n return t of </ alti // i /> --> case e' as n return t of </ alti // i />
 
 altj = K </ alphabb_kbb // bb /> </ xcc_tcc // cc /> -> u
+e = K </ t'aa // aa /> </ sbb // bb /> </ ecc // cc />
 u' = u[n |-> e] </ [alphabb_kbb |-> sbb] // bb /> </ [xcc_tcc |-> ecc] // cc />
 -------------------------------------------------------------- :: MatchData
-S |- case K </ t'aa // aa /> </ sbb // bb /> </ ecc // cc /> as n return t of </ alti // i /> --> u'
+S |- case e as n return t of </ alti // i /> --> u'
 
 altj = lit -> u
 ---------------------------------------------------------------- :: MatchLit

diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf