File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -819,14 +819,14 @@ Reference Instructions
819
819
S; F; (\I32 .\CONST ~s)~(\I32 .\CONST ~n)~(\ARRAYNEWDATA ~x~y) &\stepto & \TRAP
820
820
\\&&
821
821
\begin {array}[t]{@{}r@{~}l@{}}
822
- (\iff & \expanddt (F.\AMODULE .\MITYPES [x]) = \TARRAY ~\X {ft}^n \\
822
+ (\iff & \expanddt (F.\AMODULE .\MITYPES [x]) = \TARRAY ~\X {ft} \\
823
823
\land & s + n\cdot |\X {ft}|/8 > |S.\SDATAS [F.\AMODULE .\MIDATAS [y]].\DIDATA |)
824
824
\end {array} \\
825
825
\\[ 1 ex]
826
826
S; F; (\I32 .\CONST ~s)~(\I32 .\CONST ~n)~(\ARRAYNEWDATA ~x~y) &\stepto & (t.\CONST ~c)^n~(\ARRAYNEWFIXED ~x~n)
827
827
\\&&
828
828
\begin {array}[t]{@{}r@{~}l@{}}
829
- (\iff & \expanddt (F.\AMODULE .\MITYPES [x]) = \TARRAY ~\X {ft}^n \\
829
+ (\iff & \expanddt (F.\AMODULE .\MITYPES [x]) = \TARRAY ~\X {ft} \\
830
830
\land & t = \unpacktype (\X {ft}) \\
831
831
\land & \concat ((\bytes _{\X {ft}}(c))^n) = S.\SDATAS [F.\AMODULE .\MIDATAS [y]].\DIDATA [s \slice n\cdot |\X {ft}|/8 ] \\
832
832
\end {array} \\
You can’t perform that action at this time.
0 commit comments