		Search-engine friendly clone of the ACL2 documentation.

Defmake-self-event-generation

Defmake-self-gen-topic-name

Generate the name of the XDOC topic.

Signature
(defmake-self-gen-topic-name type) → name
Arguments: type — Guard (symbolp type).
Returns: name — Type (symbolp name).

Definitions and Theorems

Function: defmake-self-gen-topic-name

(defun defmake-self-gen-topic-name (type)
  (declare (xargs :guard (symbolp type)))
  (let ((__function__ 'defmake-self-gen-topic-name))
    (declare (ignorable __function__))
    (acl2::packn-pos (list 'make-self- type)
                     type)))

Theorem: symbolp-of-defmake-self-gen-topic-name

(defthm symbolp-of-defmake-self-gen-topic-name
  (b* ((name (defmake-self-gen-topic-name type)))
    (symbolp name))
  :rule-classes :rewrite)