		Search-engine friendly clone of the ACL2 documentation.

Process-smtlink-hints

Make-merge-function-option-lst

Add option information into func.

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

Definitions and Theorems

Function: make-merge-function-option-lst

(defun make-merge-function-option-lst (fun-opt-lst smt-func)
 (declare
      (xargs :guard (and (function-option-lst-syntax-p fun-opt-lst)
                         (func-p smt-func))))
 (let ((acl2::__function__ 'make-merge-function-option-lst))
  (declare (ignorable acl2::__function__))
  (b*
   ((fun-opt-lst (function-option-lst-syntax-fix fun-opt-lst))
    (smt-func (func-fix smt-func))
    ((unless (consp fun-opt-lst)) smt-func)
    ((cons option (cons content rest))
     fun-opt-lst)
    (new-func
     (case option
       (:formals (make-merge-formals content smt-func))
       (:returns (make-merge-returns content smt-func))
       (:level (change-func smt-func
                            :expansion-depth content))
       (:guard (make-merge-guard content smt-func))
       (:more-returns (make-merge-more-returns content smt-func)))))
   (make-merge-function-option-lst rest new-func))))

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

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