ERROR-TRIPLES

a common ACL2 programming idiom
Major Section:  STATE

When evaluation returns three values, where the first two are ordinary objects and the third is the ACL2 state, the result may be called an ``error triple''. If an error triple is (mv erp val state), we think of erp as an error flag and val as the returned value. See programming-with-state for a discussion of error triples and how to program with them.