|
|
|---|
|
|
|
|---|
Internal "instruction" data structure used by our pretty-printing algorithm.
Our pretty-printing algorithm operates in two linear passes. The first pass builds a list of printer instructions ("pinst" structures) that tell the second pass how to print. (In ACL2's pretty-printer, these structures are referred to as "ppr tuples".)
We now define the valid kinds of printer instructions. To understand these,
it is very helpful to start with print-instruction, the second
pass of pretty-printing, which follows these instructions to produce its
output. You can basically think of