|
|
|---|
|
|
|
|---|
A macro to assist in detecting runtime errors
The coi-debug::assert macro allows the user to identify runtime errors in ACL2 code. The return value of coi-debug::assert can be set by specifying a :value parameter. The failure message can be configured via the :message keyword. Note that the first argument (~x0) is the syntactic form of the test, but that additional parameters can be passed in as a list via :parameters.
Example usage pattern:
(let ((y (coi-debug::assert (test y) :value y :message "Y failed ~x0 in ~x1" :parameters (z)))) ..)