Adding user defined returns to overwrite what's already in smt-func.
(make-merge-returns-helper content) → decls
Function:
(defun make-merge-returns-helper (content) (declare (xargs :guard (argument-lst-syntax-p content))) (let ((acl2::__function__ 'make-merge-returns-helper)) (declare (ignorable acl2::__function__)) (b* ((content (argument-lst-syntax-fix content)) ((unless (consp content)) nil) ((cons first rest) content) ((cons argname (cons type (cons & hints))) first) (new-return (make-decl :name argname :type (make-hint-pair :thm type :hints (car hints))))) (cons new-return (make-merge-returns-helper rest)))))
Theorem:
(defthm decl-listp-of-make-merge-returns-helper (b* ((decls (make-merge-returns-helper content))) (decl-listp decls)) :rule-classes :rewrite)