		Search-engine friendly clone of the ACL2 documentation.

Deffold-map-event-generation

Deffold-map-gen-map-name

Generate the name of the map function for a type.

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

Definitions and Theorems

Function: deffold-map-gen-map-name

(defun deffold-map-gen-map-name (type suffix)
  (declare (xargs :guard (and (symbolp type) (symbolp suffix))))
  (let ((__function__ 'deffold-map-gen-map-name))
    (declare (ignorable __function__))
    (acl2::packn-pos (list type '- suffix)
                     suffix)))

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

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