Events to prepare proof generation.
We disable the default hints and override hints; these are implicitly local events.
We add an explicitly local event to prevent mv-nth from being expanded, which is accomplished via a system attachment.
We add an implicitly local event to set the induction depth limit to 1.
This lets generated proofs by inductions work
We add an implicitly local event to suppress various warnings. This is useful when the generated events are printed in full.
(defmacro evmac-prepare-proofs nil '(progn (set-default-hints nil) (set-override-hints nil) (local (defattach-system simplifiable-mv-nth-p constant-nil-function-arity-0)) (set-induction-depth-limit 1) (set-inhibit-warnings "disable" "double-rewrite" "free" "non-rec" "subsume" "theory" "use")))