• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
        • Vl-lint
        • Vl-server
        • Vl-gather
        • Vl-zip
        • Vl-main
        • Split-plusargs
          • Split-plusargs-exec
        • Vl-shell
        • Vl-json
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Split-plusargs

Split-plusargs-exec

Signature

(split-plusargs-exec args acc plusacc) → (mv acc plusacc)

Arguments

args — Guard (string-listp args).

acc — Guard (string-listp acc).

plusacc — Guard (string-listp plusacc).

Returns

acc — Type (string-listp acc).

plusacc — Type (string-listp plusacc).

Definitions and Theorems

Function: split-plusargs-exec

(defun split-plusargs-exec (args acc plusacc)
       (declare (xargs :guard (and (string-listp args)
                                   (string-listp acc)
                                   (string-listp plusacc))))
       (let ((__function__ 'split-plusargs-exec))
            (declare (ignorable __function__))
            (b* (((when (atom args))
                  (mv (string-list-fix acc)
                      (string-list-fix plusacc)))
                 ((cons first rest) args)
                 ((mv acc plusacc)
                  (if (and (< 0 (length first))
                           (eql (char first 0) #\+))
                      (mv acc (cons (subseq first 1 nil) plusacc))
                      (mv (cons first acc) plusacc))))
                (split-plusargs-exec rest acc plusacc))))

Theorem: string-listp-of-split-plusargs-exec.acc

(defthm string-listp-of-split-plusargs-exec.acc
        (b* (((mv ?acc ?plusacc)
              (split-plusargs-exec args acc plusacc)))
            (string-listp acc))
        :rule-classes :rewrite)

Theorem: string-listp-of-split-plusargs-exec.plusacc

(defthm string-listp-of-split-plusargs-exec.plusacc
        (b* (((mv ?acc ?plusacc)
              (split-plusargs-exec args acc plusacc)))
            (string-listp plusacc))
        :rule-classes :rewrite)