[spectec] Fix $fnat show hint (#2138)

Fix show hint for `$fnat` and update tests.

Fix `select` example in the section about instructions validation in the
spec.

Closes #2135.

Author: alessiofaieta

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.
 

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))

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))

spectec/doc/example/output/NanoWasm.pdf

@@ -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}
 $$
 

spectec/test-latex/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}`
 ............