		Search-engine friendly clone of the ACL2 documentation.

Utilities

Vl-starname

(vl-starname name) is given a string, say "foo", and return a symbol in the ACL2 package, e.g., ACL2::*foo*.

Signature
(vl-starname name) → *
Arguments: name — Guard (stringp name).

Such names are the convention for naming modules in E.

Definitions and Theorems

Function: vl-starname

(defun vl-starname (name)
  (declare (xargs :guard (stringp name)))
  (let ((__function__ 'vl-starname))
    (declare (ignorable __function__))
    (intern-in-package-of-symbol
         (implode (cons #\*
                        (str::append-chars name (list #\*))))
         'acl2::foo)))

Theorem: symbolp-of-vl-starname

(defthm symbolp-of-vl-starname
  (symbolp (vl-starname name))
  :rule-classes :type-prescription)