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