1\DOC
2
3\TYPE {apply : ('a -> 'b) -> 'a -> 'b}
4
5\SYNOPSIS
6Counts primitive inferences performed when a function is applied.
7
8\KEYWORDS
9
10\DESCRIBE
11
12The {apply} function provides a way of counting the primitive
13inferences that are performed when a function is applied to its
14argument.  The reporting of the count is done when the function
15terminates (normally, or with an exception).  The reporting also
16includes timing information about the function call.
17
18\EXAMPLE
19{
20- Count.apply (CONJUNCTS o SPEC_ALL) AND_CLAUSES;
21runtime: 0.000s,    gctime: 0.000s,     systime: 0.000s.
22Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 9; Total: 9
23val it =
24   [|- T /\ t <=> t,
25    |- t /\ T <=> t, |- F /\ t <=> F,
26    |- t /\ F <=> F,
27    |- t /\ t <=> t]: thm list
28}
29
30\FAILURE
31The call to {apply f x} will raise an exception if {f x} would.  It
32will still report elapsed time and inference counts up to the point of
33the exception being raised.
34
35\SEEALSO
36Count.thm_count.
37
38\ENDDOC
39