(parstate->char i parstate) → char+pos
Function:
(defun parstate->char (i parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (natp i))) (declare (xargs :guard (< i (parstate->chars-length parstate)))) (let ((__function__ 'parstate->char)) (declare (ignorable __function__)) (mbe :logic (if (and (parstatep parstate) (< (nfix i) (parstate->chars-length parstate))) (raw-parstate->char (nfix i) parstate) (make-char+position :char 0 :position (irr-position))) :exec (raw-parstate->char i parstate))))
Theorem:
(defthm char+position-p-of-parstate->char (b* ((char+pos (parstate->char i parstate))) (char+position-p char+pos)) :rule-classes :rewrite)