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; also see type-reasoning for additional relevant
background.
- 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 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 reasoning can assist
other reasoning engines like forward-chaining, linear-arithmetic,
and rewriting. Type-set information is stored in a type-alist data
structure; see type-reasoning for relevant basic background...
- 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.
