LD-ERROR-TRIPLES

Major Section:  MISCELLANEOUS

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. 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 3 values, the first of which is non-nil and the third of which is state, 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.