• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
          • Implementation
          • Setp
          • Right
          • Left
          • Head
            • Double-containment
            • Subset
            • Intersect
            • Insert
            • In
            • Delete
            • Union
            • Diff
            • From-list
            • To-list
            • Set-equiv
            • Sfix
            • Pick-a-point
            • Cardinality
            • Set-induct
            • Set-bi-induct
            • Emptyp
          • Soft
          • C
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Set

    Head

    Get an element of the nonempty set.

    Signature
    (head set) → *
    Arguments
    set — Guard (setp set).

    For empty trees, returns nil.

    From a user perspective, this should likely be viewed as an arbitrary element of the set, to be used only in conjunction with left and right to fold over the set. Under the hood, this is the root element of the underlying tree, which will be the unique maximum value with respect to heap<.

    Definitions and Theorems

    Function: head$inline

    (defun head$inline (set)
      (declare (xargs :guard (setp set)))
      (tree-head (sfix set)))