		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-event-generation

Deffold-map-gen-ruleset-name

Generate the name of the ruleset.

Signature
(deffold-map-gen-ruleset-name suffix) → name
Arguments: suffix — Guard (symbolp suffix).
Returns: name — Type (symbolp name).

Definitions and Theorems

Function: deffold-map-gen-ruleset-name

(defun deffold-map-gen-ruleset-name (suffix)
  (declare (xargs :guard (symbolp suffix)))
  (let ((__function__ 'deffold-map-gen-ruleset-name))
    (declare (ignorable __function__))
    (acl2::packn-pos (list 'abstract-syntax- suffix '-rules)
                     suffix)))

Theorem: symbolp-of-deffold-map-gen-ruleset-name

(defthm symbolp-of-deffold-map-gen-ruleset-name
  (b* ((name (deffold-map-gen-ruleset-name suffix)))
    (symbolp name))
  :rule-classes :rewrite)