From ebc848c6410bc0b6f505b83b95654711de68bd0e Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Mon, 30 Oct 2023 09:19:37 +0100
Subject: [PATCH] [spec] Fix prose for blocktype validation

---
 document/core/valid/types.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst
index 9366e0115..39ab9601e 100644
--- a/document/core/valid/types.rst
+++ b/document/core/valid/types.rst
@@ -130,7 +130,7 @@ Block Types
 
 * The type :math:`C.\CTYPES[\typeidx]` must be defined in the context.
 
-* Let :math:`[t_1^\ast] \toF [t_2^\ast]` be the :ref:`function type <syntax-functype>` :math:`C.\CTYPES[\typeidx]`.
+* The :ref:`expansion <aux-expand-deftype>` of :math:`C.\CFUNCS[\typeidx]` must be a :ref:`function type <syntax-functype>` :math:`\TFUNC~[t_1^\ast] \toF [t_2^\ast]`.
 
 * Then the block type is valid as :ref:`instruction type <syntax-instrtype>` :math:`[t_1^\ast] \to [t_2^\ast]`.