• Top
  • Documentation
  • Books
    • Cert.pl
    • Community-books
    • Project-dir-alist
    • Bookdata
    • Book-hash
    • Uncertified-books
    • Sysfile
    • Show-books
    • Best-practices
    • Books-reference
      • Include-book
      • Certify-book
      • Cbd
      • Set-write-ACL2x
      • Book-compiled-file
      • Add-include-book-dir
      • Pathname
      • Add-include-book-dir!
      • Full-book-name
      • Delete-include-book-dir
      • With-cbd
      • Delete-include-book-dir!
      • Set-cbd
      • Certify-book-debug
    • Where-do-i-place-my-book
    • Books-tour
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Books-reference

Delete-include-book-dir

Unlink keyword for :dir argument of ld and include-book

Example Forms:
; Remove association of a directory with :smith for include-book and ld:
(delete-include-book-dir :smith)

General Form:
(delete-include-book-dir kwd)

where kwd is a keywordp. The effect of this event is to modify the meaning of the :dir keyword argument of include-book and ld as indicated by the example above, namely by removing association of a directory with the indicated keyword for purposes of the :dir argument of include-book and ld. See add-include-book-dir for how to associate a new directory with a keyword.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

This macro is local to any books and encapsulate events in which it occurs; see add-include-book-dir for a discussion of this aspect of both macros. For non-local associations of keywords with directories, see add-include-book-dir! and delete-include-book-dir!. Note that delete-include-book-dir may only be used to remove keywords added by calls of add-include-book-dir, and delete-include-book-dir! may only be used to remove keywords added by calls of add-include-book-dir!