1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
\DOC fail
\TYPE {fail : unit -> 'a}
\SYNOPSIS
Fail with empty string.
\DESCRIBE
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
function {fail}.
\FAILURE
Always fails.
\USES
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.
\SEEALSO
\ENDDOC
|
