From 919eb10ac0186c8db1cf5b969e00d129585fd986 Mon Sep 17 00:00:00 2001 From: Wonho Shin Date: Tue, 4 Mar 2025 16:08:11 +0900 Subject: [PATCH] [spec] Fix catch validation rule --- document/core/valid/instructions.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index cb42d06288..987cbf21f8 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -2117,7 +2117,7 @@ Control Instructions * The label :math:`C.\CLABELS[l]` must be defined in the context. -* The :ref:`result type ` :math:`[t^\ast]` must be the same as :math:`C.\CLABELS[l]`. +* The :ref:`result type ` :math:`[t^\ast]` must :ref:`match ` :math:`C.\CLABELS[l]`. * Then the catch clause is valid. @@ -2125,7 +2125,7 @@ Control Instructions \frac{ \expanddt(C.\CTAGS[x]) = [t^\ast] \toF [] \qquad - C.\CLABELS[l] = [t^\ast] + C \vdashresulttypematch [t^\ast] \matchesresulttype C.\CLABELS[l] }{ C \vdashcatch \CATCH~x~l \ok } @@ -2159,13 +2159,13 @@ Control Instructions * The label :math:`C.\CLABELS[l]` must be defined in the context. -* The :ref:`result type ` :math:`C.\CLABELS[l]` must be empty. +* The :ref:`result type ` :math:`[]` must :ref:`match ` :math:`C.\CLABELS[l]`. * Then the catch clause is valid. .. math:: \frac{ - C.\CLABELS[l] = [] + C \vdashresulttypematch [] \matchesresulttype C.\CLABELS[l] }{ C \vdashcatch \CATCHALL~l \ok }