Returns the number of the most recent top-level ACL2 command.
(top-command-number-fn state) → 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.
(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))))
(defthm integerp-of-top-command-number-fn (b* ((num (top-command-number-fn state))) (integerp num)) :rule-classes :rewrite)