• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
        • Isodata
        • Simplify-defun
        • 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
          • Xdoc::apt-constructors
            • Xdoc::desc-apt-input-thm-name
            • Xdoc::desc-apt-input-thm-enable
            • Xdoc::desc-apt-input-verify-guards
            • Xdoc::apt-design-notes-ref
            • Xdoc::desc-apt-input-wrapper-to-old-name
            • Xdoc::desc-apt-input-old-to-wrapper-name
            • Xdoc::desc-apt-input-wrapper-to-old-enable
            • Xdoc::desc-apt-input-wrapper-name
            • Xdoc::desc-apt-input-old-to-wrapper-enable
            • Xdoc::desc-apt-input-old-to-new-name
            • Xdoc::desc-apt-input-old-if-new-name
            • Xdoc::desc-apt-input-new-to-old-name
            • Xdoc::desc-apt-input-wrapper-enable
            • Xdoc::desc-apt-input-old-to-new-enable
            • Xdoc::desc-apt-input-old-if-new-enable
            • Xdoc::desc-apt-input-new-to-old-enable
            • Xdoc::desc-apt-input-new-name
            • Xdoc::desc-apt-input-untranslate
            • Xdoc::desc-apt-input-old
            • Xdoc::desc-apt-input-new-enable
            • Xdoc::desc-apt-input-wrapper
          • 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
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Xdoc::apt-constructors

Xdoc::apt-design-notes-ref

Builds text that references the design notes of an APT transformation.

This should be normally put at or towards the end of the introduction section of the user documentation.

It is assumed that there is a named constant with text hyperlinked to the design notes file.

Macro: apt-design-notes-ref

(defmacro xdoc::apt-design-notes-ref (macro)
 (declare (xargs :guard (symbolp macro)))
 (b*
  ((const-design-notes (packn-pos (list "*" macro "-DESIGN-NOTES*")
                                  macro)))
  (cons
   'xdoc::p
   (cons
    '"The "
    (cons
     const-design-notes
     '(", which use "
       (xdoc::a :href
                "res/kestrel-design-notes/notation.pdf"
                "this notation")
       ", provide the mathematical concepts and template proofs
       upon which this transformation is based.
       These notes should be read alongside this reference documentation,
       which refers to them in some places."))))))