ACL2-pc::hyps
(macro)
print the hypotheses
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).
