		Search-engine friendly clone of the ACL2 documentation.

Process-smtlink-hints

Make-merge-function

Function for generating func-p of a single function hint.

Signature
(make-merge-function func smt-func) → func
Arguments: func — Guard (function-syntax-p func).; smt-func — Guard (func-p smt-func).
Returns: func — Type (func-p func).

Definitions and Theorems

Function: make-merge-function

(defun make-merge-function (func smt-func)
  (declare (xargs :guard (and (function-syntax-p func)
                              (func-p smt-func))))
  (let ((acl2::__function__ 'make-merge-function))
    (declare (ignorable acl2::__function__))
    (b* ((func (function-syntax-fix func))
         ((cons fun-name fun-opt-lst) func)
         (name fun-name))
      (make-merge-function-option-lst
           fun-opt-lst
           (change-func smt-func :name name)))))

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

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