Lex a quadruple of hexadecimal digits.
(lex-hex-quad pstate) → (mv erp quad last-pos new-pstate)
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'lex-hex-quad)) (declare (ignorable __function__)) (b* (((reterr) (irr-hex-quad) (irr-position) (irr-parstate)) ((erp hexdig1 & pstate) (lex-hexadecimal-digit pstate)) ((erp hexdig2 & pstate) (lex-hexadecimal-digit pstate)) ((erp hexdig3 & pstate) (lex-hexadecimal-digit pstate)) ((erp hexdig4 pos pstate) (lex-hexadecimal-digit pstate))) (retok (make-hex-quad :1st hexdig1 :2nd hexdig2 :3rd hexdig3 :4th hexdig4) pos pstate))))
Theorem:
(defthm hex-quad-p-of-lex-hex-quad.quad (b* (((mv acl2::?erp ?quad ?last-pos ?new-pstate) (lex-hex-quad pstate))) (hex-quad-p quad)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-lex-hex-quad.last-pos (b* (((mv acl2::?erp ?quad ?last-pos ?new-pstate) (lex-hex-quad pstate))) (positionp last-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-lex-hex-quad.new-pstate (b* (((mv acl2::?erp ?quad ?last-pos ?new-pstate) (lex-hex-quad pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-lex-hex-quad-uncond (b* (((mv acl2::?erp ?quad ?last-pos ?new-pstate) (lex-hex-quad pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-lex-hex-quad-cond (b* (((mv acl2::?erp ?quad ?last-pos ?new-pstate) (lex-hex-quad pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)