Skip to content

Commit

Permalink
[spec] Fix minor issues in local rules
Browse files Browse the repository at this point in the history
Add missing backslash on \LTYPE

Local validation doesn't need `ok`

Locals in a function have structure so need {type t} to
match the valtype
  • Loading branch information
takikawa committed Oct 31, 2023
1 parent 40f820b commit 951bda8
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions document/core/valid/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ Functions :math:`\func` are classified by :ref:`type indices <syntax-typeidx>` r
\qquad
C,\CLOCALS\,(\SET~t_1)^\ast~(\init~t)^\ast,\CLABELS~[t_2^\ast],\CRETURN~[t_2^\ast] \vdashexpr \expr : [t_2^\ast]
}{
C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : x
C \vdashfunc \{ \FTYPE~x, \FLOCALS \{\LTYPE~t\}^\ast, \FBODY~\expr \} : x
}
Expand Down Expand Up @@ -85,14 +85,14 @@ Locals
\qquad
C \vdashvaltypedefaultable t \defaultable
}{
C \vdashlocal \{ \LTYPE~t \} : \SET~t \ok
C \vdashlocal \{ \LTYPE~t \} : \SET~t
}
.. math::
\frac{
C \vdashvaltype t \ok
}{
C \vdashlocal \{ LTYPE~t \} : \UNSET~t \ok
C \vdashlocal \{ \LTYPE~t \} : \UNSET~t
}
.. note::
Expand Down

0 comments on commit 951bda8

Please sign in to comment.