• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Std/util
    • Apt
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
      • Evmac-input-hints-p
      • Function-definedness
      • Event-macro-input-processing
        • Event-macro-input-processors
          • Def-process-input-fresh-function-name
          • Evmac-process-input-hints
          • Evmac-process-input-show-only
          • Evmac-process-input-print
      • Event-macro-screen-printing
      • Evmac-input-print-p
      • Make-event-terse
      • Event-macro-applicability-conditions
      • Event-macro-results
      • Template-generators
      • Event-macro-event-generators
      • Event-macro-proof-preparation
      • Try-event
      • Restore-output?
      • Restore-output
      • Fail-event
      • Cw-event
      • Event-macro-xdoc-constructors
      • Event-macro-intro-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Event-macro-input-processors

Evmac-process-input-show-only

Process the :show-only input of an event macro.

Signature

(evmac-process-input-show-only show-only ctx state) 
  → 
(mv erp show-only$ state)

Returns

show-only$ — Type (booleanp show-only$).

This is for event macros that have a :show-only input to specify whether the event expansion should be submitted to ACL2 or just shown on the screen.

If the :show-only input, is valid, it is returned unchanged. This facilitates guard/type proofs involving this function, by obviating the need to enable this function in such proofs to establish that, if the :show-only input passes validation, then it satisfies booleanp.

Definitions and Theorems

Function: evmac-process-input-show-only

(defun
 evmac-process-input-show-only
 (show-only ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let
  ((__function__ 'evmac-process-input-show-only))
  (declare (ignorable __function__))
  (if
   (booleanp show-only)
   (value show-only)
   (er-soft+
    ctx t nil
    "The :SHOW-ONLY input must be T or NIL; ~
               but it is ~x0 instead."
    show-only))))

Theorem: booleanp-of-evmac-process-input-show-only.show-only$

(defthm booleanp-of-evmac-process-input-show-only.show-only$
        (b* (((mv ?erp ?show-only$ ?state)
              (evmac-process-input-show-only show-only ctx state)))
            (booleanp show-only$))
        :rule-classes :rewrite)