Remove the leading directory part of a path, or cause a hard error if there is any problem.
This is just a wrapper for basename that causes an error on any failure.
(defun basename!-fn (path state) (declare (xargs :stobjs (state))) (declare (xargs :guard (stringp path))) (let ((__function__ 'basename!)) (declare (ignorable __function__)) (b* (((mv err basename state) (basename path)) ((when err) (raise "Basename failed: ~@0" err) (mv "" state))) (mv basename state))))
(defthm stringp-of-basename!.basename (b* (((mv ?basename acl2::?state) (basename!-fn path state))) (stringp basename)) :rule-classes :type-prescription)