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