Name of the table that associates ATJ types to ACL2 functions.
Definition: *atj-function-type-info-table-name*
(defconst *atj-function-type-info-table-name* 'atj-function-type-info-table)