		Search-engine friendly clone of the ACL2 documentation.

Process-smtlink-hints

Make-merge-guard

Adding user defined guard to smt-func.

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

Definitions and Theorems

Function: make-merge-guard

(defun make-merge-guard (content smt-func)
  (declare (xargs :guard (and (hypothesis-syntax-p content)
                              (func-p smt-func))))
  (let ((acl2::__function__ 'make-merge-guard))
    (declare (ignorable acl2::__function__))
    (b* ((content (hypothesis-syntax-fix content))
         (smt-func (func-fix smt-func))
         ((cons thm (cons & hints-lst)) content)
         (hints (car hints-lst))
         (new-guard (make-hint-pair :thm thm :hints hints)))
      (change-func smt-func
                   :guard new-guard))))

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

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