		Search-engine friendly clone of the ACL2 documentation.

Atj-qconstants-p

Honsed-atj-qconstants

Raw constructor for honsed atj-qconstants-p structures.

Syntax:

(honsed-atj-qconstants integers rationals numbers 
                       chars strings symbols pairs next-index)

This is identical to atj-qconstants, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by std::defaggregate.

Function: honsed-atj-qconstants

(defun honsed-atj-qconstants
       (integers rationals numbers
                 chars strings symbols pairs next-index)
 (declare (xargs :guard (and (and (integer-listp integers)
                                  (no-duplicatesp integers))
                             (and (rational-listp rationals)
                                  (no-duplicatesp rationals))
                             (and (acl2-number-listp numbers)
                                  (no-duplicatesp numbers))
                             (and (character-listp chars)
                                  (no-duplicatesp chars))
                             (and (string-listp strings)
                                  (no-duplicatesp-equal strings))
                             (and (symbol-listp symbols)
                                  (no-duplicatesp-eq symbols))
                             (cons-pos-alistp pairs)
                             (posp next-index))))
 (mbe
  :logic (atj-qconstants integers rationals numbers
                         chars strings symbols pairs next-index)
  :exec
  (hons
   (hons 'integers integers)
   (hons
    (hons 'rationals rationals)
    (hons
         (hons 'numbers numbers)
         (hons (hons 'chars chars)
               (hons (hons 'strings strings)
                     (hons (hons 'symbols symbols)
                           (hons (hons 'pairs pairs)
                                 (hons (hons 'next-index next-index)
                                       nil))))))))))