• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
      • Evmac-input-hints-p
      • Evmac-input-print-p
        • Evmac-input-print-<
        • Evmac-input-print->=
        • Evmac-input-print->
        • Evmac-input-print-<=
      • Event-macro-input-processing
      • Function-definedness
      • Event-macro-screen-printing
      • 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
  • Math
  • Testing-utilities

• Evmac-input-print-p

Evmac-input-print-<

Less-than ordering on print levels.

Signature

(evmac-input-print-< x y) → yes/no

Arguments

x — Guard (evmac-input-print-p x).

y — Guard (evmac-input-print-p y).

Returns

yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: evmac-input-print-<

(defun evmac-input-print-< (x y)
  (declare (xargs :guard (and (evmac-input-print-p x)
                              (evmac-input-print-p y))))
  (let ((__function__ 'evmac-input-print-<))
    (declare (ignorable __function__))
    (case x
      ((nil)
       (or (eq y :error)
           (eq y :result)
           (eq y :info)
           (eq y :all)))
      (:error (or (eq y :result)
                  (eq y :info)
                  (eq y :all)))
      (:result (or (eq y :info) (eq y :all)))
      (:info (eq y :all))
      (:all nil))))

Theorem: booleanp-of-evmac-input-print-<

(defthm booleanp-of-evmac-input-print-<
  (b* ((yes/no (evmac-input-print-< x y)))
    (booleanp yes/no))
  :rule-classes :rewrite)