apply : ('a -> 'b) -> 'a -> 'b
STRUCTURE
Count
SYNOPSIS
Counts primitive inferences performed when a function is applied.
DESCRIPTION
The apply function provides a way of counting the primitive inferences that are performed when a function is applied to its argument. The reporting of the count is done when the function terminates (normally, or with an exception). The reporting also includes timing information about the function call.
EXAMPLE
- Count.apply (CONJUNCTS o SPEC_ALL) AND_CLAUSES;
runtime: 0.000s,    gctime: 0.000s,     systime: 0.000s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 9; Total: 9
val it =
   [|- T /\ t <=> t,
    |- t /\ T <=> t, |- F /\ t <=> F,
    |- t /\ F <=> F,
    |- t /\ t <=> t]: thm list
FAILURE
The call to apply f x will raise an exception if f x would. It will still report elapsed time and inference counts up to the point of the exception being raised.
SEEALSO
thm_count
HOL  Kananaskis-14