• 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

• Kit

Split-plusargs

Split command line arguments into plusargs and non-plusargs.

Signature

(split-plusargs args) → (mv normal plusargs)

Arguments

args — Guard (string-listp args).

Returns

normal — Non-plusargs, in order.
    Type (string-listp normal).

plusargs — Plusargs, in order, with the leading plus characters removed.
    Type (string-listp plusargs).

Definitions and Theorems

Function: split-plusargs

(defun split-plusargs (args)
       (declare (xargs :guard (string-listp args)))
       (let ((__function__ 'split-plusargs))
            (declare (ignorable __function__))
            (b* (((mv acc plusacc)
                  (split-plusargs-exec args nil nil)))
                (mv (reverse acc) (reverse plusacc)))))

Theorem: string-listp-of-split-plusargs.normal

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

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

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

Subtopics

Split-plusargs-exec