• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • 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
        • Initialize-event-user
        • Gag-mode
        • 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
    • Kestrel-utilities
    • Output-controls

    Checkpoint-info-list

    Return prover key checkpoint information programmatically.

    See checkpoint-list for relevant background and related utilities. Here we explain only how checkpoint-info-list differs from checkpoint-list. The difference is that instead of a list of clauses, it returns a list of alists each of the following form.

    ((:clause-id . clause-id)
 (:clause . clause)
 (:pushed . pushed))

    Here, clause-id is the clause-identifier of the indicated clause. The value of pushed is left undocumented here (low-level technical note: it comes from the :pushed field of the corresponding gag-info record).