• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
      • Deflist
      • Defalist
      • Memory
      • Defstructure
      • Array1
      • Utilities
        • Defloop
        • Get-option
          • Get-option-argument
          • Get-option-member
          • Get-option-check-syntax
          • Get-option-subset
          • Get-option-as-flag
          • Get-option-entries
          • Keyword-option-listp
          • Get-option-entry
          • Get-option-keywords
        • Get-guards-from-body
        • Unique-symbols
        • Pack-intern
        • Pack-string
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Get-option

Get-option-as-flag

Look for an stand-alone option, check the syntax, and return T if the option is found and NIL otherwise.

This function is for options that take no arguments, where the simple presence or absence of the option is meant to signal the user's intention.

Definitions and Theorems

Function: get-option-as-flag

(defun get-option-as-flag (ctx option option-list)
  (declare (xargs :guard (and (keywordp option)
                              (keyword-option-listp option-list))))
  (mv-let (msg flag)
          (get-option-as-flag-mv option option-list)
    (if msg (bomb ctx "~@0" msg) flag)))