		Search-engine friendly clone of the ACL2 documentation.

Deffold-reduce-event-generation

Deffoldred-gen-fold-name

Generate the name of the fold function for a type.

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

Definitions and Theorems

Function: deffoldred-gen-fold-name

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

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

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