ACL2-PC_colon__colon_SHOW-TYPE-PRESCRIPTIONS.html -- ACL2 Version 6.1

ACL2-PC::SHOW-TYPE-PRESCRIPTIONS

(macro) display the applicable type-prescription rules

Major Section:  PROOF-CHECKER-COMMANDS

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.