|
|
|---|
|
|
|
|---|
Add a trace for an FGL rule during symbolic execution
This macro has much the same interface as fgl-trace, but affects the traced rule alist in the FGL interpreter state instead of the traced rule alist stored in the ACL2 state. The latter is copied over the former at the beginning of any FGL invocation, whereas the former is used during FGL processing. Therefore, this macro is effective only during FGL processing, whereas fgl-trace is effective only outside FGL processing. This macro can be invoked from trace expressions (see fgl-trace as well as syntax-interp, syntax-bind, syntaxp, and bind-free forms.