		Search-engine friendly clone of the ACL2 documentation.

Errors

Er-soft-logic

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

See er for relevant background.

General Form:
(er-soft-logic ctx 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-logic generates :logic mode code. It works by invoking the function call (error-fms-soft-logic ctx fmt-string alist state), where alist is as in the alist argument of fmt.

For a similar utility that returns a specified error and value component of the returned error-triple, see er-soft+.