		Search-engine friendly clone of the ACL2 documentation.

Errors

Er-soft+

Print an error message and ``cause an error''

See er for relevant background.

General Form:
(er-soft+ ctx erp val fmt-string arg1 arg2 ... argk)

The form above has the same effect as

(er soft ctx fmt-string arg1 arg2 ... argk)

but unlike the latter call, the call of er-soft+ generates :logic mode code and returns the error-triple (mv erp val state) instead of always returning (mv t nil state). Note that if erp is nil then this error-triple does not signify an error.

For a simpler utility that also produces :logic mode code but always returns (mv t nil state), see er-soft-logic.