• Top
  • Documentation
  • Books
  • 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
  • Math
  • Testing-utilities

• 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