From 2067e36ea38596248af99a8037572082f267d12f Mon Sep 17 00:00:00 2001
From: Jihong Min <jihongmin63@gmail.com>
Date: Tue, 10 Mar 2026 16:31:22 +0900
Subject: [PATCH 1/2] fix: typo

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

diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec
index 6a18b8e889..60ad8dd3ce 100644
--- a/spectec/doc/semantics/il/5-reduction.spectec
+++ b/spectec/doc/semantics/il/5-reduction.spectec
@@ -18,7 +18,7 @@ rule Expand_typ/alias:
 rule Expand_typ/step:
   S |- VAR x a* => $subst_deftyp(s, dt)
   -- if (x, p* `-> OK `= inst*) <- S.TYP
-  -- if (INST `{q*} a* `= dt) <- inst*
+  -- if (INST `{q*} a'* `= dt) <- inst*
   -- Match_args: S |- a* `/ `{q*} a'* => s
 
 

From 8cd0346395317d63b4ae30bff3668a8028ed68a6 Mon Sep 17 00:00:00 2001
From: Jihong Min <jihongmin63@gmail.com>
Date: Fri, 13 Mar 2026 10:07:09 +0900
Subject: [PATCH 2/2] [spectec] elaborate subtyping rules for struct and
 variant

---
 spectec/doc/semantics/il/0-aux.spectec    | 5 +++++
 spectec/doc/semantics/il/6-typing.spectec | 8 ++++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/spectec/doc/semantics/il/0-aux.spectec b/spectec/doc/semantics/il/0-aux.spectec
index 7f322499c6..16b3bff37c 100644
--- a/spectec/doc/semantics/il/0-aux.spectec
+++ b/spectec/doc/semantics/il/0-aux.spectec
@@ -13,3 +13,8 @@ def $equiv_(syntax X, x_1*, x_2*) = false  -- otherwise
 def $transpose_(syntax X, X**) : X**
 def $transpose_(syntax X, eps^n) = eps
 def $transpose_(syntax X, (x_1 x*)*) = x_1* $transpose_(X, x**)
+
+
+def $forall(bool*) : bool 
+def $forall(eps) = true
+def $forall(bool_1 bool*) = bool_1 /\ $forall(bool*)
diff --git a/spectec/doc/semantics/il/6-typing.spectec b/spectec/doc/semantics/il/6-typing.spectec
index da62e48d33..55bb1c08dd 100644
--- a/spectec/doc/semantics/il/6-typing.spectec
+++ b/spectec/doc/semantics/il/6-typing.spectec
@@ -45,16 +45,16 @@ rule Sub_typ/struct:
   E |- t_1 <: t_2
   -- Expand_typ: E |- t_1 => STRUCT tf_1*
   -- Expand_typ: E |- t_2 => STRUCT tf_2*
-  -- (if (a `: t_2a `- `{q*} pr*) = tf_2)*
-  -- (if (a `: t_1a `- `{q*} pr*) <- tf_1*)*
+  -- (if (a `: t_2a `- `{q*} pr_2*) = tf_2)*
+  -- (if (a `: t_1a `- `{q*} pr_1*) <- tf_1* /\ $forall((pr_2 <- pr_1*)*))*
   -- (Sub_typ: E |- t_1a <: t_2a)*
 
 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 (m `: t_1a `- `{q*} pr*) = tc_1)*
-  -- (if (m `: t_2a `- `{q*} pr*) <- tc_2*)*
+  -- (if (m `: t_1a `- `{q*} pr_1*) = tc_1)*
+  -- (if (m `: t_2a `- `{q*} pr_2*) <- tc_2* /\ $forall((pr_2 <- pr_1*)*))*
   -- (Sub_typ: E |- t_1a <: t_2a)*
 
 rule Sub_typ/iter: