Add prose for typing rule of try-delegate. (#237)

- Also slightly adjusted notation to match the formal overview.
- Addressed review comments.

Author: ioannad

document/core/valid/instructions.rst

@@ -1415,20 +1415,29 @@ Control Instructions
 :math:`\TRY~\blocktype~\instr^\ast~\DELEGATE~l`
 ...............................................
 
-.. todo::
-   Add prose.
+* The label :math:`C.\CLABELS[l]` must be defined in the context.
+
+* The :ref:`block type <syntax-blocktype>` must be :ref:`valid <valid-blocktype>` as some :ref:`function type <syntax-functype>` :math:`[t_1^\ast] \to [t_2^\ast]`.
+
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_2^\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:`[t_1^\ast] \to [t_2^\ast]`.
 
 .. math::
    \frac{
      C \vdashblocktype \blocktype : [t_1^\ast] \to [t_2^\ast]
      \qquad
      C,\CLABELS\,[t_2^\ast] \vdashinstrseq \instr^\ast : [t_1^\ast]\to[t_2^\ast]
      \qquad
-     C.\CLABELS[l] = [t^\ast]
+     C.\CLABELS[l] = [t_0^\ast]
    }{
    C \vdashinstrseq \TRY~\blocktype~\instr^\ast~\DELEGATE~l : [t_1^\ast]\to[t_2^\ast]
    }
 
+.. note::
+   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
+
 
 .. _valid-throw: