|
|
|---|
|
|
|
|---|
Optional support for tracing the application of rewrite rules.
(svex-rewrite-trace rule mask args localp rhs subst) is an attachable function (see defattach) for tracing or profiling svex rewrite rules.
This is an advanced feature for SV hackers and is probably only useful if you are trying to extend or debug the svex rewriters. You may need to separately load the following book to use these attachments. (It is not included by default to avoid trust tags.)
(include-book "centaur/sv/svex/rewrite-trace" :dir :system)
Function:
(defun svex-rewrite-trace-default (rule mask args localp rhs subst) (declare (xargs :guard t) (ignorable rule mask args localp rhs subst)) nil)