Type
Disambiguation page for type-related concepts.
The word type might mean many things in ACL2.
- Built-in Types
- ACL2 can reason about and compute with certain different kinds of objects,
such as numbers, strings, characters, and conses.
See About Types for basic background on the different kinds of ACL2
objects.
- User-Defined Types
- When modeling systems with ACL2, you may often want to introduce certain
concepts as new data types. For instance, if you are modeling a network, you
might want host and connection objects. ACL2 does not directly
support introducing new types. Instead, such types are usually ``emulated'' by
introducing a new recognizer function, say hostp, and perhaps some
related constructor and accessor functions, say make-host
and host->name. Macro libraries can help to assist with introducing
common types. See for instance std/util, defdata,
or fty.
- Type Declarations
- For more efficient Common Lisp execution, ACL2 functions can be annotated
with Common Lisp type specifiers (see type-spec) that may boost
performance by reducing run-time type checking. This mechanism is integrated
with ACL2's guard mechanism, so you can prove your type declarations are
correct. See also declare and the, and also patbind-the.
- Type Prescriptions
- ACL2 includes a limited but efficient ``type-set reasoning engine
for determining whether objects are of certain built-in types. This
engine can be extended with type-prescription rules. Such rules are
often inferred automatically when new functions are introduced with defun. Type-set reasoning can assist other reasoning engines like forward-chaining, linear-arithmetic, and rewriting. Type-set
information is stored in a type-alist data structure.
- Tau
- ACL2 includes another reasoning engine, the tau-system, for
reasoning about type-like predicates. Unlike type-set, Tau can also be
used for reasoning about user-defined types, and can also carry out
certain interval arithmetic reasoning. See the introduction-to-the-tau-system for more information about Tau.
