		Search-engine friendly clone of the ACL2 documentation.

Process-smtlink-hints

Make-merge-hypothesis

Generate a hint-pair for hypo

Signature
(make-merge-hypothesis hypo) → hp
Arguments: hypo — Guard (hypothesis-syntax-p hypo).
Returns: hp — Type (hint-pair-p hp).

Definitions and Theorems

Function: make-merge-hypothesis

(defun make-merge-hypothesis (hypo)
  (declare (xargs :guard (hypothesis-syntax-p hypo)))
  (let ((acl2::__function__ 'make-merge-hypothesis))
    (declare (ignorable acl2::__function__))
    (b* ((hypo (hypothesis-syntax-fix hypo))
         ((list* thm & rest) hypo))
      (make-hint-pair :thm thm
                      :hints (car rest)))))

Theorem: hint-pair-p-of-make-merge-hypothesis

(defthm hint-pair-p-of-make-merge-hypothesis
  (b* ((hp (make-merge-hypothesis hypo)))
    (hint-pair-p hp))
  :rule-classes :rewrite)