		Search-engine friendly clone of the ACL2 documentation.

Matchresult->matchedp

Boolean flag indicating whether the regular expression matched the string

Signature
(matchresult->matchedp x) → matchedp
Arguments: x — Guard (matchresult-p x).
Returns: matchedp — Type (booleanp matchedp).

Definitions and Theorems

Function: matchresult->matchedp

(defun matchresult->matchedp (x)
  (declare (xargs :guard (matchresult-p x)))
  (let ((__function__ 'matchresult->matchedp))
    (declare (ignorable __function__))
    (and (matchresult->loc x) t)))

Theorem: booleanp-of-matchresult->matchedp

(defthm booleanp-of-matchresult->matchedp
  (b* ((matchedp (matchresult->matchedp x)))
    (booleanp matchedp))
  :rule-classes :type-prescription)

Theorem: matchresult->matchedp-of-matchresult-fix-x

(defthm matchresult->matchedp-of-matchresult-fix-x
  (equal (matchresult->matchedp (matchresult-fix x))
         (matchresult->matchedp x)))

Theorem: matchresult->matchedp-matchresult-equiv-congruence-on-x

(defthm matchresult->matchedp-matchresult-equiv-congruence-on-x
  (implies (matchresult-equiv x x-equiv)
           (equal (matchresult->matchedp x)
                  (matchresult->matchedp x-equiv)))
  :rule-classes :congruence)

Theorem: matchresult->matchedp-of-matchresult

(defthm matchresult->matchedp-of-matchresult
  (iff (matchresult->matchedp (make-matchresult :loc loc
                                                :len len
                                                :str str
                                                :backrefs backrefs))
       loc))

Theorem: natp-of-matchresult->loc

(defthm natp-of-matchresult->loc
  (iff (natp (matchresult->loc x))
       (matchresult->matchedp x))
  :rule-classes
  (:rewrite (:type-prescription
                 :corollary (implies (matchresult->matchedp x)
                                     (natp (matchresult->loc x))))))

Theorem: matchresult->loc-under-iff

(defthm matchresult->loc-under-iff
  (iff (matchresult->loc x)
       (matchresult->matchedp x)))