		Search-engine friendly clone of the ACL2 documentation.

Process-smtlink-hints

Make-merge-formals

Adding user defined formals to overwrite what's already in smt-func.

Signature
(make-merge-formals content smt-func) → func
Arguments: content — Guard (argument-lst-syntax-p content).; smt-func — Guard (func-p smt-func).
Returns: func — Type (func-p func).

Definitions and Theorems

Function: make-merge-formals

(defun make-merge-formals (content smt-func)
 (declare (xargs :guard (and (argument-lst-syntax-p content)
                             (func-p smt-func))))
 (let ((acl2::__function__ 'make-merge-formals))
  (declare (ignorable acl2::__function__))
  (b*
   ((new-formals (make-merge-formals-helper content))
    ((func f) smt-func)
    (all-formals
     (remove-duplicate-from-decl-list (append new-formals f.formals)
                                      nil)))
   (change-func f :formals all-formals))))

Theorem: func-p-of-make-merge-formals

(defthm func-p-of-make-merge-formals
  (b* ((func (make-merge-formals content smt-func)))
    (func-p func))
  :rule-classes :rewrite)