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 governorsPrint the indicated top-level hypotheses and governors. (The notion of ``governors'' is defined below.) Here,General Form: (hyps &optional hyps-indices govs-indices)
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).
