		Search-engine friendly clone of the ACL2 documentation.

Support

Split-///

Split an argument list into pre- and post-/// contents.

Definitions and Theorems

Function: split-///

(defun split-/// (ctx x)
  "Returns (mv pre-/// post-///)"
  (declare (xargs :guard t))
  (b*
    ((__function__ 'split-///)
     ((when (not x)) (mv nil nil))
     ((when (atom x))
      (raise "~x0: expected nil-terminated arguments but found ~x1."
             ctx x)
      (mv nil nil))
     ((when (eq (car x) '///))
      (mv nil (cdr x)))
     ((mv pre post) (split-/// ctx (cdr x))))
    (mv (cons (car x) pre) post)))

Theorem: true-listp-of-split-///.pre-///

(defthm true-listp-of-split-///.pre-///
  (true-listp (mv-nth 0 (split-/// ctx x))))

Theorem: true-listp-of-split-///.post-///

(defthm true-listp-of-split-///.post-///
  (implies (true-listp x)
           (true-listp (mv-nth 1 (split-/// ctx x)))))