		Search-engine friendly clone of the ACL2 documentation.

Kestrel-utilities

Top-command-number-fn

Returns the number of the most recent top-level ACL2 command.

Signature
(top-command-number-fn state) → num
Returns: num — Type (integerp num).

When a new command is accepted by the ACL2 top-level interface, the top command number is incremented and assigned to the new command.

You can see the numbers assigned to your commands with the pbt history function.

Some history functions that can change the top command number include u, ubu!, and (tsee reset-prehistory), for example.

Definitions and Theorems

Function: top-command-number-fn

(defun
 top-command-number-fn (state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let
    ((__function__ 'top-command-number-fn))
    (declare (ignorable __function__))
    (let* ((wrld (w state))
           (base-info (global-val 'command-number-baseline-info
                                  wrld))
           (command-number-base (access command-number-baseline-info
                                        base-info :current))
           (command-number-current
                (access-command-tuple-number (cddar wrld)))
           (user-command-number-current (- command-number-current
                                           command-number-base)))
          (if (integerp user-command-number-current)
              user-command-number-current 0))))

Theorem: integerp-of-top-command-number-fn

(defthm integerp-of-top-command-number-fn
        (b* ((num (top-command-number-fn state)))
            (integerp num))
        :rule-classes :rewrite)