Ld-error-triples
Determines whether a form caused an error during ld
Ld-error-triples is an ld special (see ld).
The accessor is (ld-error-triples state) and the updater is
(set-ld-error-triples val state). Ld-error-triples must be either
t or nil. The initial value of ld-error-triples is t.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co. Note that the ACL2 top-level loop (see lp) results from
an invocation of ld.
However, there are various flags that control ld's behavior and
ld-error-triples is one of them. If this variable has the value t
then when a form evaluates to an error-triple (mv erp val state)
such that erp is non-nil, then an error is deemed to have occurred.
When an error occurs in evaluating a form, ld rolls back the ACL2
world to the configuration it had at the conclusion of the last
error-free form. Then ld takes the action determined by ld-error-action.