mk_HOL_ERR

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

Creates an application of HOL_ERR.

mk_HOL_ERR provides a curried version of the HOL_ERR exception.

Failure

Never fails.

Example

   > mk_HOL_ERR "<Module>" "<function>" "<message>";
   val it = HOL_ERR (at <Module>.<function>: <message>): exn

See also

Feedback, Feedback.HOL_ERR, Feedback.mk_HOL_ERRloc