		Search-engine friendly clone of the ACL2 documentation.

Atj-qconstants-p

Atj-qconstants

Raw constructor for atj-qconstants-p structures.

Syntax:

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

This is the lowest-level constructor for atj-qconstants-p structures. It simply conses together a structure with the specified fields.

Note: It's generally better to use macros like make-atj-qconstants or change-atj-qconstants instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

The atj-qconstants-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-atj-qconstants instead.

Definition

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

Function: atj-qconstants

(defun 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))))
 (cons
  (cons 'integers integers)
  (cons
   (cons 'rationals rationals)
   (cons (cons 'numbers numbers)
         (cons (cons 'chars chars)
               (cons (cons 'strings strings)
                     (cons (cons 'symbols symbols)
                           (cons (cons 'pairs pairs)
                                 (cons (cons 'next-index next-index)
                                       nil)))))))))