• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
      • With-output
      • Summary
      • Set-inhibit-output-lst
      • Set-gag-mode
      • Goal-spec
      • Set-warnings-as-errors
      • Saving-event-data
      • Pso
      • Finalize-event-user
      • Set-inhibit-er
      • Checkpoint-list
      • Set-inhibit-warnings
      • Get-event-data
      • Set-inhibited-summary-types
      • Set-print-clause-ids
      • Set-let*-abstractionp
      • Gag-mode
      • Initialize-event-user
      • Set-raw-proof-format
      • Checkpoint-list-pretty
      • Psof
      • Set-raw-warning-format
      • Toggle-inhibit-warning
      • Toggle-inhibit-er
      • Warnings
      • Show-checkpoint-list
      • Wof
      • Psog
      • Checkpoint-info-list
      • Pso!
      • Toggle-inhibit-warning!
      • Set-duplicate-keys-action!
      • Toggle-inhibit-er!
      • Set-inhibit-warnings!
      • Set-inhibit-er!
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Output-controls

Toggle-inhibit-warning

Add or delete a warning string from the inhibit-warnings-table

General Form:
(toggle-inhibit-warning string)

where string is the name of some warning like "Subsume", "Non-rec" or "Rewrite-lambda-object".

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. It is local to the book or encapsulate form in which it occurs; see toggle-inhibit-warning! for a corresponding non-local event. Indeed, (toggle-inhibit-warning str) is equivalent to (local (toggle-inhibit-warning! str)).

The given string is added to the list of inhibited warnings if it is not there already and is deleted from the list if it is there. Case is unimportant in string. See set-inhibit-warnings.