• 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-copy-persistent

    (hons-copy-persistent x) returns a normed object that is equal to X and which will be re-normed after any calls to hons-clear.

    Logically hons-copy-persistent is the identity; we leave it enabled and would think it odd to ever prove a theorem about it.

    Under the hood, hons-copy-persistent is virtually identical to hons-copy.

    The only difference is that when hons-clear is used, any persistently normed conses are automatically re-normed, and this re-norming can be carried out more efficiently than, say, an ordinary hons-copy.

    Function: hons-copy-persistent

    (defun hons-copy-persistent (x)
      (declare (xargs :guard t))
      x)