		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-topic-name

Generate the name of the XDOC topic.

Signature
(deffoldred-gen-topic-name suffix) → name
Arguments: suffix — Guard (symbolp suffix).
Returns: name — Type (symbolp name).

Definitions and Theorems

Function: deffoldred-gen-topic-name

(defun deffoldred-gen-topic-name (suffix)
  (declare (xargs :guard (symbolp suffix)))
  (let ((__function__ 'deffoldred-gen-topic-name))
    (declare (ignorable __function__))
    (acl2::packn-pos (list 'abstract-syntax- suffix)
                     suffix)))

Theorem: symbolp-of-deffoldred-gen-topic-name

(defthm symbolp-of-deffoldred-gen-topic-name
  (b* ((name (deffoldred-gen-topic-name suffix)))
    (symbolp name))
  :rule-classes :rewrite)