		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::type-alist

(macro) display the type-alist from the current context

Examples:
(type-alist nil t nil) ; display type-alist based on governors (default)
type-alist             ; same as (type-alist nil t) -- governors only
(type-alist t t)       ; display type-alist based on conclusion and governors
(type-alist t t t)     ; as above, but also display forward-chaining report
type-alist             ; same as (type-alist nil t) -- governors only
(type-alist nil)       ; same as (type-alist nil t) -- governors only
(type-alist t)         ; same as (type-alist t nil) -- conclusion only
(type-alist nil nil)   ; based on neither conclusion nor governors
(type-alist nil t nil nil)  ; same as type-alist (default) -- governors only
(type-alist nil t nil :raw) ; governors only, raw alist format
(type-alist nil t nil t)    ; governors only, simple alist format

General Form:
(type-alist &optional concl-flg govs-flg fc-report-flg alistp)

where if govs-flg is omitted then it defaults to (not concl-flg), and each of the other optional arguments defaults to nil.

Display the current assumptions as a type-alist. Note that this display includes the result of forward chaining. When fc-report-flg is supplied a non-nil value, the display also includes a forward-chaining report; otherwise,the presence or absence of such a report is controlled by the usual global settings (see forward-chaining-reports). By default, the display is organized by type, with terms shown of each type; but when alistp is :raw then the underlying type-alist structure is shown, which is made more user-friendly when any other non-nil value of alistp is provided.

There are two basic reasons contemplated for using this command.

1. The theorem prover has failed (either outside the interactive proof-builder or using a proof-builder command such as bash or reduce and you want to debug by getting an idea of what the prover knows about the context.

a. You really are interested in the context for the current term. Include hypotheses and governors (i.e., accounting for tests of surrounding if-expressions that must be true or false) but not the current conclusion (which the theorem prover's heuristics would generally ignore for contextual information). Command:

(type-alist nil t) ; equivalently, type-alist or (type-alist nil)

b. You are not thinking in particular about the current term; you just want to get an idea of the context that the prover would build at the top-level, for forward-chaining. Incorporate the conclusion but not the governors. Command:

(type-alist t nil) ; equivalently, (type-alist t)

2. You intend to use one of the interactive proof-builder-commands that does simplification, such as s or x, and you want to see the context. Then include the surrounding if-term governors but not the goal's conclusion. Command:

(type-alist nil t) ; equivalently, type-alist or (type-alist nil)

See type-set (also see type-prescription) for information about ACL2's type system, which can assist in understanding the output of the type-alist command.