` `

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 `cons`

ing `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 `cons`

ing `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 `n`

th 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`

).