(var-is-stobj-p var world) checks whether var is currently the name of a ACL2::stobj.
Function: var-is-stobj-p
(defun var-is-stobj-p (var world) (declare (xargs :guard (and (symbolp var) (plist-worldp world)))) (consp (getprop var 'acl2::stobj nil 'acl2::current-acl2-world world)))