From 64ed2a52c3f6286541d284e12695c91410a247ff Mon Sep 17 00:00:00 2001
From: "Ioanna M. Dimitriou H" <idimitriou@igalia.com>
Date: Thu, 8 Sep 2022 14:19:57 +0200
Subject: [PATCH] Add prose for typing rule of CAUGHTadm

Fixes related .. todo:: section.

Also slightly adjusted notation to match the one in the [formal overview document](https://github.com/WebAssembly/exception-handling/blob/main/proposals/exception-handling/Exceptions-formal-overview.md).
---
 document/core/appendix/properties.rst | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst
index c9d831bc..6ffea929 100644
--- a/document/core/appendix/properties.rst
+++ b/document/core/appendix/properties.rst
@@ -646,14 +646,25 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 :math:`\CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END`
 .........................................................
 
-.. todo::
-   Add prose.
+* The :ref:`external tag value <syntax-externval>` :math:`\EVTAG~\tagaddr` must be :ref:`valid <valid-externval-tag>` with some :ref:`external tag type <syntax-externtype>` :math:`\ETTAG~[t_0^\ast] \to []`.
+
+* The :ref:`values <syntax-val>` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`.
+
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector.
+
+* Under context :math:`C'`,
+  the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t^\ast]`.
+
+* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector.
+
+* Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`.
+
 
 .. math::
    \frac{
-     S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t'^\ast]\to[]
+     S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t_0^\ast]\to[]
      \qquad
-     (val : t')^\ast
+     (val : t_0)^\ast
      \qquad
      S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast]
    }{