Programming
Programming in ACL2
This documentation topic is a parent topic under which we
include documentation topics for built-in functions, macros, and special
forms, 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 constructors like defun. A subtopic, ACL2-built-ins, contains as subtopics (displayed in a flat list) most of the
topics in the documentation hierarchy that appear under this
`programming' topic.
If you are unfamiliar with Lisp, we suggest you start by reading gentle-introduction-to-ACL2-programming.
If you are already familiar with Common Lisp (or even some other Lisp
variant), then you may find it helpful to start with the topic, introduction-to-programming-in-ACL2-for-those-who-know-lisp.
Also see debugging for utilities that can aid in programming.
Subtopics
- Defun
- Define a function symbol
- Declare
- Extra declarations that can occur in function definitions, let
bindings, and so forth.
- System-utilities
- Some built-in programming utilities pertaining to the ACL2 system
- Stobj
- Single-threaded objects or ``von Neumann bottlenecks''
- State
- The von Neumannesque ACL2 state object
- Mutual-recursion
- Define some mutually recursive functions
- Memoize
- Turn on memoization for a specified function
- Mbe
- Attach code for execution
- Io
- Input/output facilities in ACL2
- Defpkg
- Define a new symbol package
- Apply$
- Apply a badged function or tame lambda to arguments
- Loop$
- Iteration with an analogue of the Common Lisp loop macro
- Programming-with-state
- Programming using the von Neumannesque ACL2 state object
- Arrays
- ACL2 arrays and operations on them
- Characters
- Characters in ACL2 and operations on them
- Time$
- Time the evaluation of a given form
- Defmacro
- Define a macro
- Loop$-primer
- Primer for using loop$
- Fast-alists
- Alists with hidden hash tables for faster execution
- Defconst
- Define a constant
- Evaluation
- Evaluating ACL2 expressions
- Guard
- Restricting the domain of a function
- Equality-variants
- Versions of a function using different equality tests
- Compilation
- Compiling ACL2 functions
- Hons
- (hons x y) returns a normed object equal to (cons x
y).
- ACL2-built-ins
- ''Catch-all'' topic for built-in ACL2 functions
- Developers-guide
- Guide for ACL2 developers
- System-attachments
- System-level algorithms that users can modify with attachments
- Advanced-features
- Some advanced features of ACL2
- Set-check-invariant-risk
- Affect certain program-mode updates to stobjs or arrays
- Numbers
- Numbers in ACL2 and operations on them
- Efficiency
- Efficiency considerations
- Irrelevant-formals
- Formals that are used but only insignificantly
- Introduction-to-programming-in-ACL2-for-those-who-know-lisp
- Introduction to programming in ACL2 for Lisp users
- Redefining-programs
- An explanation of why we restrict redefinitions
- Lists
- Lists of objects, the classic Lisp data structure.
- Invariant-risk
- Potential slowdown for program-mode updates to stobjs
or arrays
- Errors
- Support for causing runtime errors, breaks, assertions, etc.
- Defabbrev
- A convenient form of macro definition for simple expansions
- Conses
- A cons is an ordered pair. In ACL2, data structures like
lists, alists, etc., are made up of conses.
- Alists
- Operations on association lists, which bind keys to values.
- Set-register-invariant-risk
- Avoid invariant-risk checking for specified functions
- Strings
- Strings are atomic objects that contain character sequences,
like "Hello World".
- Program-wrapper
- Avoiding expensive guard checks using program-mode functions
- Get-internal-time
- Runtime vs. realtime in ACL2 timings
- Basics
- Basic control structures for programming like if and
cond, binding operators like let and flet, multiple-value
constructs like mv, and so forth.
- Packages
- Collections of symbols that act as namespaces.
- Oracle-eval
- Evaluate a term and return its result, logically obtained by reading
the state's oracle.
- Defmacro-untouchable
- Define an ``untouchable'' macro
- <<
- A total ordering on ACL2 objects.
- Primitive
- Primitive functions built into ACL2 without definitions
- Revert-world
- Evaluate without (ultimately) changing the world
- Unmemoize
- Turn off memoization for the specified function
- Set-duplicate-keys-action
- Control action for macro calls with duplicate keyword arguments
- Symbols
- Symbols in ACL2 and operations on them
- Def-list-constructor
- Define function that constructs a list, just by giving the length and
how to compute the Nth element in terms of the formals and index.
- Easy-simplify-term
- A simple interface for simplifying a term, perhaps under a hypothesis
and equivalence context, and with optional guidance from a hint.
- Defiteration
- Define a simple for-loop-style iteration, counting up over some
range.
- Fake-oracle-eval
- fake-oracle-eval is the function run by default when oracle-eval is invoked.
- Defopen
- A simple event generator that creates a theorem by finding out what a
term simplifies to under some hyp and with some hint.
- Sleep
- Sleep for some number of seconds
