		Search-engine friendly clone of the ACL2 documentation.

Constraint-rule

Make-constraint-rule

Basic constructor macro for constraint-rule structures.

Syntax

(make-constraint-rule [:thmname <thmname>] 
                      [:lit-alist <lit-alist>] 
                      [:syntaxp <syntaxp>])

This is the usual way to construct constraint-rule structures. It simply conses together a structure with the specified fields.

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-constraint-rule

(defmacro make-constraint-rule (&rest args)
  (std::make-aggregate 'constraint-rule
                       args
                       '((:thmname) (:lit-alist) (:syntaxp))
                       'make-constraint-rule
                       nil))

Function: constraint-rule

(defun constraint-rule (thmname lit-alist syntaxp)
  (declare (xargs :guard (and (symbolp thmname)
                              (pseudo-term-subst-p lit-alist)
                              (pseudo-termp syntaxp))))
  (declare (xargs :guard t))
  (let ((__function__ 'constraint-rule))
    (declare (ignorable __function__))
    (b* ((thmname (mbe :logic (acl2::symbol-fix thmname)
                       :exec thmname))
         (lit-alist (mbe :logic (pseudo-term-subst-fix lit-alist)
                         :exec lit-alist))
         (syntaxp (mbe :logic (pseudo-term-fix syntaxp)
                       :exec syntaxp)))
      (cons thmname (cons lit-alist syntaxp)))))