		Search-engine friendly clone of the ACL2 documentation.

Regex-exact

Make-regex-exact

Basic constructor macro for regex-exact structures.

Syntax

(make-regex-exact [:str <str>])

This is the usual way to construct regex-exact structures. It simply conses together a structure with the specified fields.

This macro generates a new regex-exact structure from scratch. See also change-regex-exact, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-regex-exact

(defmacro make-regex-exact (&rest args)
  (std::make-aggregate 'regex-exact
                       args '((:str))
                       'make-regex-exact
                       nil))

Function: regex-exact

(defun regex-exact (str)
  (declare (xargs :guard (stringp str)))
  (declare (xargs :guard t))
  (let ((__function__ 'regex-exact))
    (declare (ignorable __function__))
    (b* ((str (mbe :logic (acl2::str-fix str)
                   :exec str)))
      (cons :exact (list str)))))