		Search-engine friendly clone of the ACL2 documentation.

Errors

Ctx

Context object for error messages

Calls of er, such as (er soft ctx ...), take a context argument, typically called ctx, for the initial part of the message: "ACL2 Error in". If ctx is nil, only "ACL2 Error:" is printed for that initial part of the message. Otherwise, the string printed after "in" depends on the form of that context, as follows. (See ctxp for the definition of a valid context.)

If ctx is a symbol, print it with fmt using "~x".
If ctx is a pair whose car is a symbol, use fmt to print "(~x0 ~x1 ...)", with #\0 and #\1 bound respectively to the car and cdr of ctx. Exception: if the car is a member of the value of constant *fmt-ctx-spacers*, then a space is printed after the left parenthesis. That explains why there is a space, for example, in "( DEFUN" in error messages starting with:
```
ACL2 Error in ( DEFUN FOO ...):
```
Otherwise, print ctx with fmt using "~@".