		Search-engine friendly clone of the ACL2 documentation.

Defun-inst-implementation

Check-qrewrite-rule-funvars

Check if the rewrite rule of a quantifier second-order function, or of an instance of it, depends exactly on the same function variables that the matrix of the function depends on.

Signature
(check-qrewrite-rule-funvars fun wrld) → err-msg?
Arguments: fun — Guard (symbolp fun).; wrld — Guard (plist-worldp wrld).
Returns: err-msg? — A maybe-msgp.

When a quantifier second-order function, or an instance thereof, is introduced, the submitted event form first introduces the function, and then checks whether its rewrite rule depends exactly on the same function variables that the matrix of the function depends on. The following code performs this check.

If the check is satisfied, nil is returned. Otherwise, an error message is returned.

This check is relevant when the rewrite rule is a custom one. Otherwise, it is a redundant check.

Definitions and Theorems

Function: check-qrewrite-rule-funvars

(defun check-qrewrite-rule-funvars (fun wrld)
 (declare (xargs :guard (and (symbolp fun)
                             (plist-worldp wrld))))
 (let ((__function__ 'check-qrewrite-rule-funvars))
  (declare (ignorable __function__))
  (let* ((rule-name (defun-sk-rewrite-name fun wrld))
         (rule-body (formula rule-name nil wrld))
         (fun-matrix (defun-sk-matrix fun wrld)))
   (if (set-equiv (funvars-of-term rule-body wrld)
                  (funvars-of-term fun-matrix wrld))
       nil
    (msg
     "The custom rewrite rule ~x0 must have ~
            the same function variables as the function's matrix ~x1.~%"
     rule-body fun-matrix)))))