About Types

The universe of ACL2 objects includes objects of many different
types. For example,

Numbers such as 3, -22/7, #c(3 5/2) .Characters such as #\A, #\a, #\Space .Strings such as "This is a string." .Symbols such as 'abc, 'smith::abc .Conses (or Ordered Pairs) such as '((a . 1) (b . 2)) .

When proving theorems it is important to know the types of object returned
by a term. ACL2 uses a complicated heuristic algorithm, called `type-set` `type-prescription`

ACL2 is an ``untyped'' logic in the sense that the syntax is not typed: It
is legal to apply a function symbol of n arguments to any n terms, regardless
of the types of the argument terms. Thus, it is permitted to write such odd
expressions as

To make theorem proving easier in ACL2, the axioms actually define a value
for such terms. The value of

You might immediately wonder about our claim that ACL2 is Common Lisp,
since **guards**. We will discuss guards later in the Walking Tour. However,
many new users simply ignore the issue of guards entirely and that is what we
recommend for now.

You should now return to