Split up the rest of a define line into macro arguments and macro text.
(vl-split-define-text text config) → (mv successp formals body)
Function:
(defun vl-split-define-text (text config) (declare (xargs :guard (and (vl-echarlist-p text) (vl-loadconfig-p config)))) (let ((__function__ 'vl-split-define-text)) (declare (ignorable __function__)) (b* (((unless (and (consp text) (eql (vl-echar->char (car text)) #\())) (mv t nil (vl-echarlist-fix text)))) (vl-parse-define-formal-arguments (cdr text) config (vl-echar->loc (car text))))))
Theorem:
(defthm booleanp-of-vl-split-define-text.successp (b* (((mv ?successp ?formals ?body) (vl-split-define-text text config))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-define-formallist-p-of-vl-split-define-text.formals (b* (((mv ?successp ?formals ?body) (vl-split-define-text text config))) (vl-define-formallist-p formals)) :rule-classes :rewrite)
Theorem:
(defthm vl-echarlist-p-of-vl-split-define-text.body (implies (force (vl-echarlist-p text)) (b* (((mv ?successp ?formals ?body) (vl-split-define-text text config))) (vl-echarlist-p body))) :rule-classes :rewrite)