Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

check : ('a -> bool) -> 'a -> 'a

SYNOPSIS

Checks that a value satisfies a predicate.

DESCRIPTION

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

FAILURE CONDITIONS

check p x fails with Failure "check" if the predicate p yields false when applied to the value x.

EXAMPLE

  # check is_var `x:bool`;;
  val it : term = `x`
  # check is_var `x + 2`;;
  Exception: Failure "check".

USES

Can be used to filter out candidates from a set of terms, e.g. to apply theorem-tactics to assumptions with a certain pattern.

SEE ALSO

can.