ACL2-PC::HYPS

(macro) print the hypotheses
Major Section:  PROOF-CHECKER-COMMANDS

Examples:
hyps               -- print all (top-level) hypotheses
(hyps (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4
(hyps (1 3) t)     -- print hypotheses 1 and 3 and all governors

General Form: (hyps &optional hyps-indices govs-indices)

Print the indicated top-level hypotheses and governors. (The notion of ``governors'' is defined below.) Here, hyps-indices and govs-indices should be lists of indices of hypotheses and governors (respectively), except that the atom t may be used to indicate that one wants all hypotheses or governors (respectively).

The list of ``governors'' is defined as follows. Actually, we define here the notion of the governors for a pair of the form <term, address>]; we're interested in the special case where the term is the conclusion and the address is the current address. If the address is nil, then there are no governors, i.e., the list of governors is nil. If the term is of the form (if x y z) and the address is of the form (2 . rest) or (3 . rest), then the list of governors is the result of consing x or its negation (respectively) onto the list of governors for the pair <y, rest> or the pair <z, rest> (respectively). If the term is of the form (implies x y) and the address is of the form (2 . rest), then the list of governors is the result of consing x onto the list of governors for the pair <y, rest>. Otherwise, the list of governors for the pair <term, (n . rest)> is exactly the list of governors for the pair <argn, rest> where argn is the nth argument of term.

If all goals have been proved, a message saying so will be printed. (as there will be no current hypotheses or governors!).

The hyps command never causes an error. It ``succeeds'' (in fact its value is t) if the arguments (when supplied) are appropriate, i.e. either t or lists of indices of hypotheses or governors, respectively. Otherwise it ``fails'' (its value is nil).