format_ERR

Feedback.format_ERR : error_record -> string

Maps argument record of HOL_ERR to a string.

The format_ERR function maps the argument of an application of HOL_ERR to a string. It is the default function used by ERR_to_string.

Failure

Never fails.

Example

> print
  (format_ERR {origin_structure = "Foo",
              origin_function = "bar",
              message = "incomprehensible input"});
Exception- Type error in function application.
   Function: format_ERR : hol_error -> string
   Argument:
      {origin_structure = "Foo", origin_function = "bar",
        message = "incomprehensible input"} :
      {message: string,
        origin_function: string, origin_structure: string}
   Reason:
      Can't unify hol_error to
         {message: string,
           origin_function: string, origin_structure: string}
         (Incompatible types)
Fail "Static Errors" raised

See also

Feedback, Feedback.ERR_to_string, Feedback.format_MESG, Feedback.format_WARNING