PROGRAMMING

programming in ACL2

Major Section:  ACL2 Documentation

This documentation topic is a parent topic under which we include documentation topics for built-in functions, macros, and special forms (see acl2-built-ins) as well as topics for notions important to programming with ACL2. If you don't find what you're looking for, see the Index or see individual topics that may be more directly appropriate; for example, see events for top-level event constructorsr like defun.

Some Related Topics

ACL2-BUILT-INS -- built-in ACL2 functions
ACL2-CUSTOMIZATION -- file of initial commands for ACL2 to run at startup
ACL2-USER -- a package the ACL2 user may prefer
ARRAYS -- an introduction to ACL2 arrays
CERTIFY-BOOK -- how to produce a certificate for a book
COMP -- compile some ACL2 functions
COMP-GCL -- compile some ACL2 functions leaving .c and .h files
COMPILATION -- compiling ACL2 functions
DECLARE -- declarations
DEFCONST -- define a constant
DEFPKG -- define a new symbol package
DEFUN -- define a function symbol
EQUALITY-VARIANTS -- versions of a function using different equality tests
IGNORABLE -- See declare.
IGNORE -- See declare.
IRRELEVANT-FORMALS -- formals that are used but only insignificantly
MUTUAL-RECURSION -- define some mutually recursive functions
OPTIMIZE -- See declare.
REDEFINING-PROGRAMS -- an explanation of why we restrict redefinitions
SET-BOGUS-MUTUAL-RECURSION-OK -- allow unnecessary ``mutual recursion''
SET-COMPILE-FNS -- have each function compiled as you go along.
SET-IGNORE-OK -- allow unused formals and locals without an ignore or ignorable declaration
SET-IRRELEVANT-FORMALS-OK -- allow irrelevant formals in definitions
SET-STATE-OK -- allow the use of STATE as a formal parameter
SINGLE-THREADED-OBJECTS -- See stobj.
STATE -- the von Neumannesque ACL2 state object
TIME$ -- time an evaluation
TIME-TRACKER -- display time spent during specified evaluation
TRACE -- tracing functions in ACL2
TYPE -- See declare.
ZERO-TEST-IDIOMS -- how to test for 0

PROGRAMMING

Some Related Topics

ACL2-BUILT-INS -- built-in ACL2 functions

ACL2-CUSTOMIZATION -- file of initial commands for ACL2 to run at startup

ACL2-USER -- a package the ACL2 user may prefer

ARRAYS -- an introduction to ACL2 arrays

CERTIFY-BOOK -- how to produce a certificate for a book

COMP -- compile some ACL2 functions

COMP-GCL -- compile some ACL2 functions leaving .c and .h files

COMPILATION -- compiling ACL2 functions

DECLARE -- declarations

DEFCONST -- define a constant

DEFPKG -- define a new symbol package

DEFUN -- define a function symbol

EQUALITY-VARIANTS -- versions of a function using different equality tests

IGNORABLE -- See declare.

IGNORE -- See declare.

IRRELEVANT-FORMALS -- formals that are used but only insignificantly

MUTUAL-RECURSION -- define some mutually recursive functions

OPTIMIZE -- See declare.

REDEFINING-PROGRAMS -- an explanation of why we restrict redefinitions

SET-BOGUS-MUTUAL-RECURSION-OK -- allow unnecessary ``mutual recursion''

SET-COMPILE-FNS -- have each function compiled as you go along.

SET-IGNORE-OK -- allow unused formals and locals without an ignore or ignorable declaration

SET-IRRELEVANT-FORMALS-OK -- allow irrelevant formals in definitions

SET-STATE-OK -- allow the use of STATE as a formal parameter

SINGLE-THREADED-OBJECTS -- See stobj.

STATE -- the von Neumannesque ACL2 state object

TIME$ -- time an evaluation

TIME-TRACKER -- display time spent during specified evaluation

TRACE -- tracing functions in ACL2

TYPE -- See declare.

ZERO-TEST-IDIOMS -- how to test for 0

SET-IGNORE-OK -- allow unused formals and locals without an `ignore` or `ignorable` declaration