►Dracula: Reference Manual
▼1 ACL2
Version: 4.1.4
  ← prev  up  next → 

1 ACL2

Applicative Common Lisp (ACL) is the executable component of the ACL2 programming language. This section documents the syntax and behavior of ACL programs as simulated by Dracula. For more information on the ACL2 language, see the ACL2 webpage.

    1.1 Data Types

    1.2 Expressions

    1.3 Events and Definitions

    1.4 Functions and Macros

      1.4.1 Booleans

      1.4.2 Symbols

      1.4.3 Strings

      1.4.4 Characters

      1.4.5 Rational and Complex Arithmetic

      1.4.6 Bitwise Operations

      1.4.7 Ordinal Arithmetic

      1.4.8 Lists

      1.4.9 Association Lists

      1.4.10 Sets

      1.4.11 Trees

      1.4.12 Sequences

      1.4.13 IO

    1.5 Theorem Prover Controls

    1.6 ACL2 Books

      1.6.1 "data-structures/list-theory"

      1.6.2 "data-structures/structures"

    1.7 Unsupported

  ← prev  up  next →