Version: 4.1

Dracula: ACL2 in DrScheme

    1 Dracula

    2 Applicative Common Lisp

      2.1 Data Types

      2.2 Expressions

      2.3 Events and Definitions

      2.4 Functions and Macros

        2.4.1 Booleans

        2.4.2 Symbols

        2.4.3 Strings

        2.4.4 Characters

        2.4.5 Rational and Complex Arithmetic

        2.4.6 Bitwise Operations

        2.4.7 Ordinal Arithmetic

        2.4.8 Lists

        2.4.9 Association Lists

        2.4.10 Sets

        2.4.11 Trees

        2.4.12 Sequences

        2.4.13 IO

      2.5 Theorem Prover Controls

      2.6 Unsupported

    3 Books and Teachpacks

      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"

    Index