2.5. Literals🔗

true
false
0
42
1_000
0b1010
0o755
0xCAFE
-42                  // unary minus applied to 42
3.1415               // exact mathematical real
6.02e23              // exact decimal with an exponent
"hello\nworld"
255 bv 8             // bitvector value 255, width 8
<?>                  // deterministic unknown
<??>                 // nondeterministic unknown

Natural tokens may be decimal, binary (0b/0B), octal (0o/0O), or hexadecimal (0x/0X). Underscores may separate digits, and every underscore run must be followed by a valid digit. Integer syntax is nonnegative: a negative value is unary - applied to a natural.

A decimal token must contain a decimal point or an e/E exponent. Forms such as 1., 1.25, 1e6, and 1.25e-3 denote exact mathematical real values — not float64.

String literals use double quotes. The implemented escapes are \\, \", \', \r, \n, \t, \xHH, and \uHHHH. A backslash followed by a newline and further non-newline whitespace is a string gap and contributes no character. Other characters, including an unescaped newline, are kept literally; an unknown or incomplete escape is a parse error.