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.
(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)