• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
      • Acre-internals
      • Parse-and-match-regex
      • Match-regex
      • Parse
      • Matchresult->matchedp
      • Match
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Prime-field-constraint-systems
    • Proof-checker-array
    • Soft
    • Rp-rewriter
    • Farray
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Bigmem
    • Regex
    • ACL2-programming-language
    • Java
    • C
    • Jfkr
    • X86isa
    • Equational
    • Cryptography
    • Where-do-i-place-my-book
    • Json
    • Built-ins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Acre
• Matchresult

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)))