The number of prover steps most recently taken

For discussions of prover step limits, See set-prover-step-limit and see with-prover-step-limit.

The summary printed for an event typically includes a line showing the prover steps counted, for example as follows.

Prover steps counted: 7240

The value of the form `thm` or `certify-book` — regardless of
whether or not summary output is inhibited (see set-inhibit-output-lst
and see set-inhibited-summary-types). In particular, the value is
updated (typically to `table` events, even when no
summary is printed; for example, the value is updated to `logic``program``set-prover-step-limit`.

The value of

nil , if no prover steps were taken, e.g., with(thm (equal x x)) ; else,the (positive) number of steps taken, if the number of steps did not exceed the starting limit; else,

the negative of the starting limit.

Note that the ``most recently completed event'' in this sense includes compound events. Consider the following example.

(progn (thm (equal (append (append x y) z) (append x y z))) (thm (equal (car (cons x y)) x)))

The summaries show (in some ACL2 versions, at least) 435 steps for the
first call of

Prover steps counted: 435 Prover steps counted: More than 5 Prover steps counted: More than 440

Since the most recently completed event is the

We conclude with two remarks for advanced users who wish to invoke

Remark 1. Suppose that you want to write a utility that takes some action
based on the number of prover steps performed by the first event that is
generated within a sequence of events, for example the number of prover steps
taken to admit

(progn (defun f1 ...) (defun f2 ...))

A solution is to record the steps taken by the first `defun` before
executing subsequent events, as follows (see make-event).

(progn (defun f1 ...) (make-event (pprogn (f-put-global 'my-step-count (last-prover-steps state) state) (value '(value-triple nil)))) (defun f2 ...))

Remark 2. It is possible to write utilities that are treated as events for purposes of the discussion above; that is, their calls can be
followed by evaluating `prove$` in community-book