inferences

Count.inferences : ('a -> 'b) -> 'a -> 'b

Counts primitive inferences performed when a function is applied.

The inferences 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).

Example

> Count.apply (CONJUNCTS o SPEC_ALL) AND_CLAUSES;
runtime: 0.00001s,    gctime: 0.00000s,     systime: 0.00000s.
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 inferences f x will raise an exception if f x would. It will still report inference counts up to the point of the exception being raised.

See also

Count.apply