An ACL2 representation of contextual knowledge

See type-reasoning for basic background on type reasoning in ACL2.

The ACL2 prover maintains many structures that need not be understood by
the user. One of these, the *type-alist* structure, is usually in this
category. But some utilities refer to the type-alist, so we summarize it
here.

A type-alist is an association list, each element of which is of the form
`(u ts . ttree)`, where `*TS-typ*` to denote the type described by `typ`, and for
complements they use `(TS-COMPLEMENT *TS-typ*)`. For example, a
context in which the terms `(p x y)`,

----- Terms with type *TS-T*: (NO-DUPLICATESP-EQUAL Y) ----- Terms with type (TS-COMPLEMENT *TS-NIL*): (P X Y) ----- Terms with type *TS-NON-NEGATIVE-INTEGER*: X -----

These lines says that `(p x y)` is not the symbol `natp`).

ACL2 computes a type-alist based on contextual information including the
hypotheses of the current goal (technically: the negations of the literals in
the goal that are not currently being rewritten), forward-chaining
from those literals, and the surrounding tests in calls of