• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
        • Function-definedness
        • Event-macro-input-processing
        • Event-macro-screen-printing
        • Make-event-terse
        • Event-macro-applicability-conditions
          • Evmac-input-hints-p
          • Event-macro-applicability-condition-utilities
            • Evmac-appcond-theorem
            • Evmac-appcond-theorem-list
            • Evmac-appcondp
              • Evmac-appcond
              • Make-evmac-appcond
              • Change-evmac-appcond
              • Make-honsed-evmac-appcond
              • Honsed-evmac-appcond
              • Evmac-appcond->name
              • Evmac-appcond->formula
            • Evmac-ensure-no-extra-hints
            • Make-evmac-appcond?
            • Evmac-appcond-theorems-no-extra-hints
            • Evmac-appcond-listp
        • 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
  • Event-macro-applicability-condition-utilities

Evmac-appcondp

Recognize applicability conditions.

(evmac-appcondp x) is a std::defaggregate of the following fields.

  • name — Invariant (keywordp name).
  • formula — Invariant (pseudo-termp formula).

Source link: evmac-appcondp

We represent an applicability condition as an aggregate.

The first field is a keyword that names the applicabiilty condition. This keyword should be the one shown in the user documentation of the event macro, and in progress or error messages on the screen when the event macro runs. The keyword may be one of a fixed finite set of possibilities, or could be calculated dynamically (e.g. to include a numeric index), based on the specifics of the event macro.

The second field is the formula (a term) that must be proved for the applicability condition to be satisfied.

More fields might be added in the future.

Subtopics

Evmac-appcond
Raw constructor for evmac-appcondp structures.
Make-evmac-appcond
Constructor macro for evmac-appcondp structures.
Change-evmac-appcond
A copying macro that lets you create new evmac-appcondp structures, based on existing structures.
Make-honsed-evmac-appcond
Constructor macro for honsed evmac-appcondp structures.
Honsed-evmac-appcond
Raw constructor for honsed evmac-appcondp structures.
Evmac-appcond->name
Access the name field of a evmac-appcondp structure.
Evmac-appcond->formula
Access the formula field of a evmac-appcondp structure.