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