Basic constructor macro for regex-case-sens structures.
(make-regex-case-sens [:pat <pat>] [:case-insens <case-insens>])
This is the usual way to construct regex-case-sens structures. It simply conses together a structure with the specified fields.
This macro generates a new regex-case-sens structure from scratch. See also change-regex-case-sens, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-regex-case-sens (&rest args) (std::make-aggregate 'regex-case-sens args '((:pat) (:case-insens)) 'make-regex-case-sens nil))
Function:
(defun regex-case-sens (pat case-insens) (declare (xargs :guard (and (regex-p pat) (booleanp case-insens)))) (declare (xargs :guard t)) (let ((__function__ 'regex-case-sens)) (declare (ignorable __function__)) (b* ((pat (mbe :logic (regex-fix pat) :exec pat)) (case-insens (mbe :logic (acl2::bool-fix case-insens) :exec case-insens))) (cons :case-sens (list pat case-insens)))))