Skip to content

Commit

Permalink
Update document/core/valid/matching.rst
Browse files Browse the repository at this point in the history
Add note for seemingly identical premise and conclusion

Co-authored-by: Andreas Rossberg <rossberg@mpi-sws.org>
  • Loading branch information
f52985 and rossberg authored Jan 10, 2025
1 parent de8aaec commit 61561e9
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions document/core/valid/matching.rst
Original file line number Diff line number Diff line change
Expand Up @@ -591,6 +591,11 @@ A :ref:`tag type <syntax-tagtype>` :math:`\deftype_1` matches :math:`\deftype_2`
C \vdashtagtypematch \deftype_1 \matchestagtype \deftype_2
}
.. note::
Although the conclusion of this rule looks identical to its premise,
they in fact describe different relations:
the premise invokes subtyping on defined types,
while the conclusion defines it on tag types that happen to be expressed as defined types.

.. index:: external type, function type, table type, memory type, global type
.. _match-externtype:
Expand Down

0 comments on commit 61561e9

Please sign in to comment.