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.
(check-qrewrite-rule-funvars fun wrld) → err-msg?
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,
This check is relevant when the rewrite rule is a custom one. Otherwise, it is a redundant check.
Function:
(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)))))