		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Get-charset

Signature
(get-charset str) → pat
Arguments: str — Guard (stringp str).
Returns: pat — Type (implies pat (regex-p pat)).

Definitions and Theorems

Function: get-charset

(defun get-charset (str)
  (declare (xargs :guard (stringp str)))
  (let ((__function__ 'get-charset))
    (declare (ignorable __function__))
    (b* (((mv err charset &)
          (parse-charset (str::cat (lstrfix str) "]")
                         0))
         ((when err)
          (raise "Error parsing charset: ~x0 -- ~s1"
                 (lstrfix str)
                 err)))
      charset)))

Theorem: return-type-of-get-charset

(defthm return-type-of-get-charset
  (b* ((pat (get-charset str)))
    (implies pat (regex-p pat)))
  :rule-classes :rewrite)

Theorem: get-charset-of-str-fix-str

(defthm get-charset-of-str-fix-str
  (equal (get-charset (acl2::str-fix str))
         (get-charset str)))

Theorem: get-charset-streqv-congruence-on-str

(defthm get-charset-streqv-congruence-on-str
  (implies (acl2::streqv str str-equiv)
           (equal (get-charset str)
                  (get-charset str-equiv)))
  :rule-classes :congruence)