mk_HOL_ERR

Feedback.mk_HOL_ERR : string -> string -> string -> exn

Creates an application of HOL_ERR.

mk_HOL_ERR provides a curried interface to the standard HOL_ERR exception; experience has shown that this is often more convenient.

Failure

Never fails.

Example

- mk_HOL_ERR "Module" "function" "message"

> val it = HOL_ERR : exn

- print(exn_to_string it);

Exception raised at Module.function:
message
> val it = () : unit

See also

Feedback, Feedback.HOL_ERR, Feedback.error_record