		Search-engine friendly clone of the ACL2 documentation.

Constraint-tuple-p

Make-constraint-tuple

Constructor macro for constraint-tuple-p structures.

Syntax:

(make-constraint-tuple [:rule <rule>] 
                       [:existing-lits <existing-lits>] 
                       [:matching-lit <matching-lit>] 
                       [:common-vars <common-vars>] 
                       [:existing-vars <existing-vars>] 
                       [:sig-table <sig-table>])

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

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

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

Definition

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

Macro: make-constraint-tuple

(defmacro make-constraint-tuple (&rest args)
  (std::make-aggregate 'constraint-tuple
                       args
                       '((:rule)
                         (:existing-lits)
                         (:matching-lit)
                         (:common-vars)
                         (:existing-vars)
                         (:sig-table))
                       'make-constraint-tuple
                       nil))