Version: 4.1

3 Books and Teachpacks

(include-book "<basename>")

(include-book "<basename>" :dir :system)

(include-book "<basename>" :dir :teachpacks)

The include-book form imports definitions from a file called a book. Dracula supports three variants.

  (include-book "my-path/my-book")

Without a :dir option, Dracula adds a ".lisp" extension to the base name and attempts to load a file relative to the current directory. In the case above, the program must reside in a directory with a "my-path" subdirectory containing a book named "my-book.lisp".

Books must be valid Dracula programs; they must start with (in-package "ACL2"); and they must contain only events, no top-level expressions.

  (include-book "my-path/my-book" :dir :system)

This variant loads a book from the system directory included with an ACL2 installation. Dracula simulates only a couple of the definitions from these books, but allows other books to be included for theorem proving purposes. See below for the supported books.

  (include-book "my-path/my-book" :dir :teachpack)

The third variant loads one of the books provided with Dracula, called teachpacks. These books make use of DrScheme features such as interactive animations and other i/o, and are also reflected in the ACL2 logic.

    3.1 ACL2 Books

      3.1.1 "data-structures/list-theory"

      3.1.2 "data-structures/structures"

    3.2 Dracula Teachpacks

      3.2.1 "audio"

      3.2.2 "avl-rational-keys"

      3.2.3 "binary-io-utilities"

      3.2.4 "doublecheck"

      3.2.5 "io-utilities"

      3.2.6 "list-utilities"

      3.2.7 "rand"

      3.2.8 "testing"

      3.2.9 "world"