Disabledp
Determine whether a given name or rune is disabled
Examples:
:disabledp foo ; returns a list of all disabled runes whose base
; symbol is foo (see rune)
(disabledp 'foo) ; same as above (i.e., :disabledp foo)
:disabledp (:rewrite bar . 1) ; returns t if the indicated rune is
; disabled, else nil
(disabledp (:rewrite bar . 1)); same as immediately above
(disabledp '(:definition binary-append))
; returns t if the indicated definition is disabled, else nil
(disabledp '(:d append))
; same as above
Also see pr, which gives much more information about the rules
associated with a given event.
Disabledp takes one argument, which is a symbol, a rune, or a
runic abbreviation such as (:d append) (see theories). In the
former case it returns the list of disabled runes associated with that name,
in the sense that the rune's ``base symbol'' is that name (see rune)
or, if the event named is a defmacro event, then the list of disabled
runes associated with the function corresponding to that macro name, if
any (see macro-aliases-table). In the other cases, where the argument
is a rune or a runic abbreviation for a rune, disabledp returns
t if the rune is disabled, and nil otherwise.
Remark for users of the break-rewrite utility. Inside the
:brr loop, the computation performed by disabledp takes
place with respect to the state of the proof that is currently underway,
rather than the global state. For example, if you break while the prover is
working on Subgoal 3, and the hints supplied for the proof specify
("Subgoal 3" :in-theory (disable foo)), then disabled will
return the runes associated with foo, regardless of whether or not those
runes are disabled globally.
