rocq/backend/Text.v
Text as the backend builds it: a list of parts, each a string, which the driver writes one after another. A printer takes the parts that follow it and puts its own in front, as asm.pl's grammar rules do with their difference lists, so no text is ever copied to be joined: SQLite's assembly is about 100 MB.
The newline and tab characters, which Rocq's string notation cannot write.
The digits 0 to 9. A definition of its own, like ten below, because the extracted code builds a list or a number again each time it meets one written inside a function.
The digit d, for 0 to 9.
The digits of n, which is not negative, in front of acc. The fuel is a bound on the number of digits.
Numbers below this have at most 18 decimal digits.
A bound on the number of decimal digits of n: 18 for the numbers below 10^18, which are nearly all a compile prints, and the number of binary digits for the others.
n in decimal, with a minus sign when it is negative, as Prolog writes an integer.