|
|
|---|
|
|
|
|---|
Associates a function symbol with a macro for printing user-level terms
Examples: ACL2 !>(untrans-table (w state)) ((BINARY-+ + . T) (BINARY-* * . T) (BINARY-APPEND APPEND . T) (BINARY-LOGAND LOGAND . T) (BINARY-LOGIOR LOGIOR . T) (BINARY-LOGXOR LOGXOR . T) (BINARY-LOGEQV LOGEQV . T) (BINARY-POR POR . T) (BINARY-PAND PAND . T))
See table for a general discussion of tables.
See add-macro-fn for a more general discussion of this table and for a way to associate a macro name with a function name in theory events.