display the type-alist from the current context
Major Section: PROOF-CHECKER-COMMANDS
Examples: (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) ; display type-alist without considering ; conclusion or governors General Form: (type-alist &optional concl-flg govs-flg fc-report-flg)where if
govs-flg
is omitted then it defaults to (not concl-flg)
,
and concl-flg
and fc-report-flg
default 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).
There are two basic reasons contemplated for using this command.
1. The theorem prover has failed (either outside the proof-checker or using a
proof-checker 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 proof-checker-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.