		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Charset-char-regex

Signature
(charset-char-regex x) → pat
Returns: pat — Type (implies pat (regex-p pat)).

Definitions and Theorems

Function: charset-char-regex

(defun charset-char-regex (x)
  (declare (xargs :guard t))
  (let ((__function__ 'charset-char-regex))
    (declare (ignorable __function__))
    (cdr (assoc x *charset-table*))))

Theorem: return-type-of-charset-char-regex

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