		Search-engine friendly clone of the ACL2 documentation.

Process-smtlink-hints

Merge-functions

Merging function hints into smt-hint.

Signature
(merge-functions content hint) → new-hint
Arguments: content — Guard (function-lst-syntax-p content).; hint — Guard (smtlink-hint-p hint).
Returns: new-hint — Type (smtlink-hint-p new-hint).

Definitions and Theorems

Function: merge-functions

(defun merge-functions (content hint)
  (declare (xargs :guard (and (function-lst-syntax-p content)
                              (smtlink-hint-p hint))))
  (let ((acl2::__function__ 'merge-functions))
    (declare (ignorable acl2::__function__))
    (b* ((hint (smtlink-hint-fix hint))
         (content (function-lst-syntax-fix content))
         ((unless (consp content)) hint)
         ((cons first rest) content)
         (name (car first))
         ((smtlink-hint h) hint)
         (exist? (hons-get name h.fast-functions))
         (smt-func (if exist? (cdr exist?) (make-func)))
         (new-func-lst (cons (make-merge-function first smt-func)
                             h.functions))
         (new-hint (change-smtlink-hint hint
                                        :functions new-func-lst)))
      (merge-functions rest new-hint))))

Theorem: smtlink-hint-p-of-merge-functions

(defthm smtlink-hint-p-of-merge-functions
  (b* ((new-hint (merge-functions content hint)))
    (smtlink-hint-p new-hint))
  :rule-classes :rewrite)