• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Mutual-recursion
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Loop$-primer
        • Fast-alists
        • Defmacro
        • Defconst
        • Evaluation
        • Guard
        • Equality-variants
        • Compilation
        • 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
          • ACL2-built-ins
          • Developers-guide
          • System-attachments
          • Advanced-features
          • Set-check-invariant-risk
          • Numbers
          • Irrelevant-formals
          • Efficiency
          • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
          • Redefining-programs
          • Lists
          • Invariant-risk
          • Errors
          • Defabbrev
          • Conses
          • Alists
          • Set-register-invariant-risk
          • Strings
          • Program-wrapper
          • Get-internal-time
          • Basics
          • Packages
          • Defmacro-untouchable
          • Primitive
          • <<
          • Revert-world
          • Set-duplicate-keys-action
          • Unmemoize
          • Symbols
          • Def-list-constructor
          • Easy-simplify-term
          • Defiteration
          • Defopen
          • Sleep
        • Start-here
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Hons
    • ACL2-built-ins

    Hons-summary

    (hons-summary) prints basic information about the sizes of the tables in the current Hons Space.

    Logically, hons-summary just returns nil; we leave it enabled and would think it odd to ever prove a theorem about it.

    Under the hood, this function gathers and prints some basic information about the sizes of the tables in the Hons Space.

    This information may be useful for deciding if you want to garbage collect using functions such as hons-clear or hons-wash. It may also be useful for determining good initial sizes for the Hons Space hash tables for your particular computation; see hons-resize. For information about fast-alists, see fast-alist-summary.

    Function: hons-summary

    (defun hons-summary
           nil (declare (xargs :guard t))
           nil)