diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst
index d92dd7d197..eef8989d19 100644
--- a/document/core/valid/instructions.rst
+++ b/document/core/valid/instructions.rst
@@ -43,7 +43,7 @@ In both cases, the unconstrained types or type sequences can be chosen arbitrari
 
    and
 
-   $${instr*: (CONST F64 $fnat(64, 1)) (CONST F64 $fnat(64, 2)) (CONST F64 $fnat(64, 3)) (SELECT)}
+   $${instr*: (CONST F64 $fnat(64, 1)) (CONST F64 $fnat(64, 2)) (CONST I32 3) (SELECT)}
 
    are valid, with ${:t} in the typing of ${:SELECT} being instantiated to ${:I32} or ${:F64}, respectively.
 
diff --git a/specification/wasm-3.0/1.1-syntax.values.spectec b/specification/wasm-3.0/1.1-syntax.values.spectec
index b1bce66333..670a329c90 100644
--- a/specification/wasm-3.0/1.1-syntax.values.spectec
+++ b/specification/wasm-3.0/1.1-syntax.values.spectec
@@ -60,7 +60,7 @@ syntax f64 = fN(`64)
 def $fzero(N) : fN(N) hint(show $(+0))
 def $fzero(N) = POS (SUBNORM 0)
 
-def $fnat(N, nat) : fN(N)  hint(show $(+%))
+def $fnat(N, nat) : fN(N)  hint(show $(+%2))
 def $fnat(N, n) = POS (NORM n 0)
 
 def $fone(N) : fN(N)  hint(show $(+1))
diff --git a/specification/wasm-latest/1.1-syntax.values.spectec b/specification/wasm-latest/1.1-syntax.values.spectec
index b1bce66333..670a329c90 100644
--- a/specification/wasm-latest/1.1-syntax.values.spectec
+++ b/specification/wasm-latest/1.1-syntax.values.spectec
@@ -60,7 +60,7 @@ syntax f64 = fN(`64)
 def $fzero(N) : fN(N) hint(show $(+0))
 def $fzero(N) = POS (SUBNORM 0)
 
-def $fnat(N, nat) : fN(N)  hint(show $(+%))
+def $fnat(N, nat) : fN(N)  hint(show $(+%2))
 def $fnat(N, n) = POS (NORM n 0)
 
 def $fone(N) : fN(N)  hint(show $(+1))
diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index 4722e81f4d..68bdcbc000 100644
Binary files a/spectec/doc/example/output/NanoWasm.pdf and b/spectec/doc/example/output/NanoWasm.pdf differ
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index d6d5e0903b..ab0c4bf934 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -2533,7 +2533,7 @@ $$
 
 $$
 \begin{array}[t]{@{}lcl@{}l@{}}
-{+N} & = & {+((1 + n \cdot {2^{{-M}}}) \cdot {2^{0}})} \\
+{+n} & = & {+((1 + n \cdot {2^{{-M}}}) \cdot {2^{0}})} \\
 \end{array}
 $$
 
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index b7183fb062..9fa5e5369a 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -21242,7 +21242,7 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i
 1. Return :math:`({+((0 + 0 \cdot {2^{{-M}}}) \cdot {2^{e}})})`.
 
 
-:math:`{+N}`
+:math:`{+n}`
 ............