ACL2-pc::show-type-prescriptions
(macro)
display the applicable type-prescription rules
Example:
show-type-prescriptions
General Form:
(show-type-prescriptions &optional rule-id)
Display type-prescription rules that apply to the current subterm.
If rule-id is supplied and is a name (non-nil symbol) or a
:rewrite or :definition rune, then only the
corresponding rewrite rule(s) will be displayed. In each case, the display
will point out when a rule is currently disabled (in the interactive
environment). Also see type-prescription.
