1\DOC assert
2
3\TYPE {assert : ('a -> bool) -> 'a -> 'a}
4
5\SYNOPSIS
6Checks that a value satisfies a predicate.
7
8\DESCRIBE
9{assert p x} returns {x} if the application {p x} yields {true}. Otherwise,
10{assert p x} fails.
11
12\FAILURE
13{assert p x} fails with exception {HOL_ERR} if the predicate {p} yields
14{false} when applied to the value {x}. If the application {p x} raises an
15exception {e}, then {assert p x} raises {e}.
16
17\EXAMPLE
18{
19- null [];
20> val it = true : bool
21
22- assert null ([]:int list);
23> val it = [] : int list
24
25- null [1];
26> false : bool
27
28- assert null [1];
29! Uncaught exception:
30! HOL_ERR <poly>
31}
32
33\SEEALSO
34Lib.can, Lib.assert_exn.
35
36\ENDDOC
37