• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
        • Simplify-defun
        • Isodata
        • Tailrec
        • Schemalg
        • Restrict
        • Expdata
        • Casesplit
        • Simplify-term
        • Simplify-defun-sk
        • Parteval
        • Solve
        • Wrap-output
        • Propagate-iso
        • Simplify
        • Finite-difference
        • Drop-irrelevant-params
        • Copy-function
        • Lift-iso
        • Rename-params
        • Utilities
          • Defaults-table
            • Set-default-input-wrapper-to-old-name
            • Set-default-input-old-to-wrapper-name
            • Set-default-input-old-to-new-name
            • Set-default-input-new-to-old-name
            • Set-default-input-old-if-new-name
            • Set-default-input-wrapper-to-old-enable
            • Set-default-input-old-to-wrapper-enable
            • Set-default-input-old-to-new-enable
            • Set-default-input-new-to-old-enable
            • Set-default-input-wrapper-enable
            • Set-default-input-old-if-new-enable
            • Get-default-input-wrapper-to-old-name
            • Get-default-input-wrapper-to-old-enable
            • Get-default-input-old-to-wrapper-name
            • Get-default-input-old-to-wrapper-enable
            • Get-default-input-old-to-new-name
            • Get-default-input-old-to-new-enable
            • Get-default-input-old-if-new-name
            • Get-default-input-old-if-new-enable
            • Get-default-input-new-to-old-name
            • Get-default-input-new-to-old-enable
            • Get-default-input-wrapper-enable
            • *defaults-table-name*
          • Xdoc::apt-constructors
          • Input-processors
          • Transformation-table
          • Find-base-cases
          • Untranslate-specifier-utilities
          • Print-specifier-utilities
          • Hints-specifier-utilities
        • Simplify-term-programmatic
        • Simplify-defun-sk-programmatic
        • Simplify-defun-programmatic
        • Simplify-defun+
        • Common-options
        • Common-concepts
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Utilities

Defaults-table

APT defaults table.

This is analogous to the ACL2 defaults table, but it is specific to APT. It contains information about various defaults that affect certain aspects of the behavior of APT transformations.

Support for more defaults will be added as needed.

We provide event macros to change the defaults. These should be used instead of modifying the table directly.

Internally, each default is represented by a pair in the table. The key is always a keyword, while the value depends on the default.

Subtopics

Set-default-input-wrapper-to-old-name

Set the default :wrapper-to-old-name input of APT transformations.

Set-default-input-old-to-wrapper-name

Set the default :old-to-wrapper-name input of APT transformations.

Set-default-input-old-to-new-name

Set the default :old-to-new-name input of APT transformations.

Set-default-input-new-to-old-name

Set the default :new-to-old-name input of APT transformations.

Set-default-input-old-if-new-name

Set the default :old-if-new-name input of APT transformations.

Set-default-input-wrapper-to-old-enable

Set the default :wrapper-to-old-enable input of APT transformations.

Set-default-input-old-to-wrapper-enable

Set the default :old-to-wrapper-enable input of APT transformations.

Set-default-input-old-to-new-enable

Set the default :old-to-new-enable input of APT transformations.

Set-default-input-new-to-old-enable

Set the default :new-to-old-enable input of APT transformations.

Set-default-input-wrapper-enable

Set the default :wrapper-enable input of APT transformations.

Set-default-input-old-if-new-enable

Set the default :old-if-new-enable input of APT transformations.

Get-default-input-wrapper-to-old-name

Get the default :wrapper-to-old-name input of APT transformations.

Get-default-input-wrapper-to-old-enable

Get the default :wrapper-to-old-enable input of APT transformations.

Get-default-input-old-to-wrapper-name

Get the default :old-to-wrapper-name input of APT transformations.

Get-default-input-old-to-wrapper-enable

Get the default :old-to-wrapper-enable input of APT transformations.

Get-default-input-old-to-new-name

Get the default :old-to-new-name input of APT transformations.

Get-default-input-old-to-new-enable

Get the default :old-to-new-enable input of APT transformations.

Get-default-input-old-if-new-name

Get the default :old-if-new-name input of APT transformations.

Get-default-input-old-if-new-enable

Get the default :old-if-new-enable input of APT transformations.

Get-default-input-new-to-old-name

Get the default :new-to-old-name input of APT transformations.

Get-default-input-new-to-old-enable

Get the default :new-to-old-enable input of APT transformations.

Get-default-input-wrapper-enable

Get the default :wrapper-enable input of APT transformations.

*defaults-table-name*

Name of the table of APT defaults.