Adding user-defined more-return theorems.
(make-merge-more-returns content smt-func) → func
Function:
(defun make-merge-more-returns (content smt-func) (declare (xargs :guard (and (hypothesis-lst-syntax-p content) (func-p smt-func)))) (let ((acl2::__function__ 'make-merge-more-returns)) (declare (ignorable acl2::__function__)) (b* ((content (hypothesis-lst-syntax-fix content)) (smt-func (func-fix smt-func)) ((func f) smt-func) ((unless (consp content)) smt-func) ((cons first rest) content) ((cons thm (cons & hints-lst)) first) (hints (car hints-lst)) (new-more-return (make-hint-pair :thm thm :hints hints)) (new-func (change-func smt-func :more-returns (cons new-more-return f.more-returns)))) (make-merge-more-returns rest new-func))))
Theorem:
(defthm func-p-of-make-merge-more-returns (b* ((func (make-merge-more-returns content smt-func))) (func-p func)) :rule-classes :rewrite)