Lex a quadruple of hexadecimal digits.
(lex-hex-quad parstate) → (mv erp quad last-pos new-parstate)
This is called when we expect four hexadecimal digits, so we call lex-hexadecimal-digit four times. We return the position of the last one.
Function:
(defun lex-hex-quad (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'lex-hex-quad)) (declare (ignorable __function__)) (b* (((reterr) (irr-hex-quad) (irr-position) parstate) ((erp hexdig1 & parstate) (lex-hexadecimal-digit parstate)) ((erp hexdig2 & parstate) (lex-hexadecimal-digit parstate)) ((erp hexdig3 & parstate) (lex-hexadecimal-digit parstate)) ((erp hexdig4 pos parstate) (lex-hexadecimal-digit parstate))) (retok (make-hex-quad :1st hexdig1 :2nd hexdig2 :3rd hexdig3 :4th hexdig4) pos parstate))))
Theorem:
(defthm hex-quad-p-of-lex-hex-quad.quad (b* (((mv acl2::?erp ?quad ?last-pos ?new-parstate) (lex-hex-quad parstate))) (hex-quad-p quad)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-hex-quad.last-pos (b* (((mv acl2::?erp ?quad ?last-pos ?new-parstate) (lex-hex-quad parstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-hex-quad.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?quad ?last-pos ?new-parstate) (lex-hex-quad parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-hex-quad-uncond (b* (((mv acl2::?erp ?quad ?last-pos ?new-parstate) (lex-hex-quad parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-hex-quad-cond (b* (((mv acl2::?erp ?quad ?last-pos ?new-parstate) (lex-hex-quad parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)