• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
        • Defmapping
        • Defenum
        • Add-io-pairs
        • Defalist
        • Defmapappend
        • Returns-specifiers
        • Defarbrec
        • Defines
        • Define-sk
        • Error-value-tuples
        • Defmax-nat
        • Defmin-int
        • Deftutorial
        • Extended-formals
        • Defrule
        • Defval
        • Defsurj
        • Defiso
        • Defconstrained-recognizer
        • Deffixer
        • Defmvtypes
        • Defconsts
        • Defthm-unsigned-byte-p
        • Support
          • Extract-keywords
          • Dumb-string-sublis
          • Raise
          • Look-up-return-vals
          • Logic-mode-p
          • Look-up-wrapper-args
          • Look-up-formals
          • Legal-kwds-p
          • Split-///
            • Keyword-legality
            • Getarg+
            • Var-is-stobj-p
            • Look-up-guard
            • Getarg
            • Cons-listp
            • Tuplep
            • Tuple-listp
            • Ends-with-period-p
          • Defthm-signed-byte-p
          • Defthm-natp
          • Defund-sk
          • Defmacro+
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Std/strings
        • Std/osets
        • Std/io
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • 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)))))