File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -110,6 +110,7 @@ Execution
110110=============================================== ===============================================================================
111111Construct Judgement
112112=============================================== ===============================================================================
113- :ref: `Instruction <exec-instr >` :math: `S;F;\instr ^\ast \stepto S';F';{\instr '}^\ast `
114- :ref: `Expression <exec-expr >` :math: `S;F;\expr \stepto S';F';\expr '`
113+ :ref: `Instruction <exec-instr >` :math: `S;F;\instr ^\ast \stepto ^{\act ^\ast } S';F';{\instr '}^\ast `
114+ :ref: `Expression <exec-expr >` :math: `S;F;\expr \stepto ^{\act ^\ast } S';F';\expr '`
115+ :ref: `Configuration <syntax-reduction >` :math: `\config \stepto ^{\evt } \config '`
115116=============================================== ===============================================================================
Original file line number Diff line number Diff line change @@ -4210,8 +4210,8 @@ An :ref:`expression <syntax-expr>` is *evaluated* relative to a :ref:`current <e
42104210The value :math: `\val ` is the result of the evaluation.
42114211
42124212.. math ::
4213- S; F; \instr ^\ast \stepto S'; F'; \instr '^\ast
4214- \qquad (\iff S; F; \instr ^\ast ~\END \stepto S'; F'; \instr '^\ast ~\END )
4213+ S; F; \instr ^\ast \stepto ^{ \act ^ \ast } S'; F'; \instr '^\ast
4214+ \qquad (\iff S; F; \instr ^\ast ~\END \stepto ^{ \act ^ \ast } S'; F'; \instr '^\ast ~\END )
42154215
42164216 .. note ::
42174217 Evaluation iterates this reduction rule until reaching a value.
You can’t perform that action at this time.
0 commit comments