►Dracula: ACL2 in Dr Scheme
▼2 Applicative Common Lisp
Version: 4.1.1
  ← prev  up  next → 

2 Applicative Common Lisp

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.

    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

  ← prev  up  next →