(cst2ast-string-literal-contents contents double-quoted-p) → elements
Function:
(defun cst2ast-string-literal-contents (contents double-quoted-p) (declare (xargs :guard (and (abnf::tree-listp contents) (booleanp double-quoted-p)))) (let ((__function__ 'cst2ast-string-literal-contents)) (declare (ignorable __function__)) (b* (((unless (and (abnf::tree-listp contents) (booleanp double-quoted-p))) (reserrf "bad call to cst2ast-string-literal-contents")) ((when (endp contents)) nil) (first-string-element (cst2ast-string-literal-content (car contents) double-quoted-p)) ((unless (string-elementp first-string-element)) (reserrf "problem in cst2ast-string-literal-contents")) ((unless (listp (cdr contents))) (reserrf "problem in cst2ast-string-literal-contents 2")) (rest-string-elements (cst2ast-string-literal-contents (cdr contents) double-quoted-p)) ((unless (string-element-listp rest-string-elements)) (reserrf "problem in cst2ast-string-literal-contents 3"))) (cons first-string-element rest-string-elements))))
Theorem:
(defthm string-element-list-resultp-of-cst2ast-string-literal-contents (b* ((elements (cst2ast-string-literal-contents contents double-quoted-p))) (string-element-list-resultp elements)) :rule-classes :rewrite)