Fail with empty string.
In HOL Light, the class of exceptions Failure "string" is used consistently.
This makes it easy to catch all HOL-related exceptions by a Failure _ pattern
without accidentally catching others. In general, the failure can be generated
by failwith "string", but the special case of an empty string is bound to the
- FAILURE CONDITIONS
Useful when there is no intention to propagate helpful information about the
cause of the exception, for example because you know it will be caught and
handled without discrimination.
- SEE ALSO