From fcd0720517734fdbb399180afc4c4aefe3c68050 Mon Sep 17 00:00:00 2001
From: Sukyoung Ryu <sukyoung.ryu@gmail.com>
Date: Sat, 21 Feb 2026 10:58:46 +0900
Subject: [PATCH 1/2] Update 6-typing.spectec

---
 spectec/doc/semantics/il/6-typing.spectec | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/spectec/doc/semantics/il/6-typing.spectec b/spectec/doc/semantics/il/6-typing.spectec
index 203767cac3..7c18705624 100644
--- a/spectec/doc/semantics/il/6-typing.spectec
+++ b/spectec/doc/semantics/il/6-typing.spectec
@@ -53,8 +53,8 @@ rule Sub_typ/variant:
   E |- t_1 <: t_2
   -- Expand_typ: E |- t_1 => VARIANT tc_1*
   -- Expand_typ: E |- t_2 => VARIANT tc_2*
-  -- (if (a `: t_1a `- `{q*} pr*) = tc_1)*
-  -- (if (a `: t_2a `- `{q*} pr*) <- tc_2*)*
+  -- (if (m `: t_1a `- `{q*} pr*) = tc_1)*
+  -- (if (m `: t_2a `- `{q*} pr*) <- tc_2*)*
   -- (Sub_typ: E |- t_1a <: t_2a)*
 
 rule Sub_typ/iter:
@@ -311,7 +311,7 @@ rule Ok_exp/STR:
   ;; Note: premises need not hold!
 
 rule Ok_exp/SEL:
-  E |- SEL e n : $subst_typ({EXP (x_i, e_i)^n}, t_n)
+  E |- SEL e n : $subst_typ({EXP (x_i, e_i)^(i<n)}, t_n)
   -- Ok_exp: E |- e : TUP (x `: t)*
   -- if t_n = t*[n]
   -- (if x_i = x*[i])^(i<n)
@@ -460,7 +460,7 @@ rule Ok_sym/RANGE:
 rule Ok_sym/ITER:
   E |- ITER g it (x `<- e)* : ITER t it'
   -- Ok_iter: E |- it : it' -| E'
-  -- (Ok_exp: E |- e' : ITER t' it')*
+  -- (Ok_exp: E |- e : ITER t' it')*
   -- Ok_sym: E ++ {EXP (x, t')*} ++ E' |- g : t
   -- Ok_typ: E |- t : OK
 
@@ -502,8 +502,8 @@ rule Ok_prem/LET:
 rule Ok_prem/ITER:
   E |- ITER pr it (x `<- e)* : OK
   -- Ok_iter: E |- it : it' -| E'
-  -- (Ok_exp: E |- e' : ITER t' it')*
-  -- Ok_prem: E ++ {EXP (x, t_x)*} ++ E' |- pr : OK
+  -- (Ok_exp: E |- e : ITER t' it')*
+  -- Ok_prem: E ++ {EXP (x, t')*} ++ E' |- pr : OK
 
 
 rule Ok_prems:

From 9d21cd791a6d50e18a84aa61436420a863ab6588 Mon Sep 17 00:00:00 2001
From: Sukyoung Ryu <sukyoung.ryu@gmail.com>
Date: Sat, 21 Feb 2026 17:18:33 +0900
Subject: [PATCH 2/2] revert the change

---
 spectec/doc/semantics/il/6-typing.spectec | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spectec/doc/semantics/il/6-typing.spectec b/spectec/doc/semantics/il/6-typing.spectec
index 7c18705624..f8dc09b417 100644
--- a/spectec/doc/semantics/il/6-typing.spectec
+++ b/spectec/doc/semantics/il/6-typing.spectec
@@ -311,7 +311,7 @@ rule Ok_exp/STR:
   ;; Note: premises need not hold!
 
 rule Ok_exp/SEL:
-  E |- SEL e n : $subst_typ({EXP (x_i, e_i)^(i<n)}, t_n)
+  E |- SEL e n : $subst_typ({EXP (x_i, e_i)^n}, t_n)
   -- Ok_exp: E |- e : TUP (x `: t)*
   -- if t_n = t*[n]
   -- (if x_i = x*[i])^(i<n)