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
26
27
28
29
30
31
|
\DOC check
\TYPE {check : ('a -> bool) -> 'a -> 'a}
\SYNOPSIS
Checks that a value satisfies a predicate.
\DESCRIBE
{check p x} returns {x} if the application {p x} yields {true}. Otherwise,
{check p x} fails.
\FAILURE
{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.
\SEEALSO
can.
\ENDDOC
|
