Print some warnings in a ``raw'', s-expression format
General Forms: (set-raw-warning-format t) :set-raw-warning-format t (set-raw-warning-format nil) :set-raw-warning-format nil
This command affects
; default format ACL2 Warning [Subsume] in ( DEFTHM APP-COMMUTES ...): A newly proposed :REWRITE rule generated from APP-COMMUTES probably subsumes the previously added :REWRITE rule APP-CONS, in the sense that the new rule will now probably be applied whenever the old rule would have been. ; raw format (:WARNING "Subsume" ((:CTX (DEFTHM . APP-COMMUTES)) (:NEW-RULE APP-COMMUTES) (:RULE-CLASS-NEW :REWRITE) (:RULE-CLASS-OLD :REWRITE) (:SUBSUMED-RULES (APP-CONS))))
As illustrated above, it is typical that in the raw format, the
To obtain the current raw-warning-format (
NOTE: Only a few commonly-occurring classes of warnings are shown differently in raw-warning-format.