assert

Lib.assert : ('a -> bool) -> 'a -> 'a

Checks that a value satisfies a predicate.

assert p x returns x if the application p x yields true. Otherwise, assert p x fails.

Failure

assert p x fails with exception HOL_ERR if the predicate p yields false when applied to the value x. If the application p x raises an exception e, then assert p x raises e.

Example

> null [];
val it = true: bool

> assert null ([]:int list);
val it = []: int list

> null [1];
val it = false: bool

> assert null [1];
Exception- HOL_ERR (at Lib.assert: predicate not true) raised

See also

Lib.can, Lib.assert_exn