Size of the parsing state.
(parsize parstate) → size
This is a synonym of parstate->size at this point. It was slightly more elaborate when parstate was defined via fty::defprod.
Function:
(defun parsize (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parsize)) (declare (ignorable __function__)) (parstate->size parstate)))
Theorem:
(defthm natp-of-parsize (b* ((size (parsize parstate))) (natp size)) :rule-classes (:rewrite :type-prescription))
Theorem:
(defthm parsize-of-initparstate (equal (parsize (init-parstate nil gcc parstate)) 0))
Theorem:
(defthm parsize-of-parstate-fix-parstate (equal (parsize (parstate-fix parstate)) (parsize parstate)))
Theorem:
(defthm parsize-parstate-equiv-congruence-on-parstate (implies (parstate-equiv parstate parstate-equiv) (equal (parsize parstate) (parsize parstate-equiv))) :rule-classes :congruence)