• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
        • Memoize
        • Fast-alists
        • Hons
          • Normed
          • Hons-note
          • Hons-resize
          • Hons-wash
          • Hons-clear
          • Hons-copy
          • Maybe-wash-memory
          • Hons-equal
          • Hons-summary
          • Hons-equal-lite
          • Hons-sublis
          • Hons-wash!
          • Hons-clear!
            • Hons-copy-persistent
          • Set-max-mem
          • Hons-enabled
          • Unmemoize
          • Number-subtrees
        • Events
        • Parallelism
        • History
        • Programming
        • Operational-semantics
        • Real
        • Start-here
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Hons
    • ACL2-built-ins

    Hons-clear!

    A version of hons-clear for parallel execution

    This function is only of interest to ACL2(p) users; see parallelism, because for ACL2 it suffices to use hons-clear. However, if parallel execution is enabled (see set-parallel-execution), as it is by default in ACL2(p), then hons-clear may be a no-op (other than to print a warning), in order to avoid thread-unsafe behavior. If you are not concerned about thread safety, for example when you want to call hons-clear directly in the top-level loop, you can use hons-clear!, which does not check for parallelism violations. However, hons-clear! requires a trust tag; see defttag.