Adding user defined returns to overwrite what's already in smt-func.
(make-merge-returns content smt-func) → func
Function:
(defun make-merge-returns (content smt-func) (declare (xargs :guard (and (argument-lst-syntax-p content) (func-p smt-func)))) (let ((acl2::__function__ 'make-merge-returns)) (declare (ignorable acl2::__function__)) (b* ((new-return (make-merge-returns-helper content)) ((func f) smt-func) (all-returns (remove-duplicate-from-decl-list (append new-return f.returns) nil))) (change-func f :returns all-returns))))
Theorem:
(defthm func-p-of-make-merge-returns (b* ((func (make-merge-returns content smt-func))) (func-p func)) :rule-classes :rewrite)