		Search-engine friendly clone of the ACL2 documentation.

Atj-qconstants-p

Make-atj-qconstants

Constructor macro for atj-qconstants-p structures.

Syntax:

(make-atj-qconstants [:integers <integers>] 
                     [:rationals <rationals>] 
                     [:numbers <numbers>] 
                     [:chars <chars>] 
                     [:strings <strings>] 
                     [:symbols <symbols>] 
                     [:pairs <pairs>] 
                     [:next-index <next-index>])

This is our preferred way to construct atj-qconstants-p structures. It simply conses together a structure with the specified fields.

This macro generates a new atj-qconstants-p structure from scratch. See also change-atj-qconstants, which can "change" an existing structure, instead.

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

Definition

This is an ordinary make- macro introduced by std::defaggregate.

Macro: make-atj-qconstants

(defmacro make-atj-qconstants (&rest args)
  (std::make-aggregate 'atj-qconstants
                       args
                       '((:integers)
                         (:rationals)
                         (:numbers)
                         (:chars)
                         (:strings)
                         (:symbols)
                         (:pairs)
                         (:next-index))
                       'make-atj-qconstants
                       nil))