		Search-engine friendly clone of the ACL2 documentation.

Database

Flex->name

Name of a sum, list, alist, transparent sum, set, or omap type, given the information associated to the type.

Signature
(flex->name info) → name
Returns: name — Type (symbolp name).

Definitions and Theorems

Function: flex->name

(defun flex->name (info)
  (declare (xargs :guard t))
  (let ((__function__ 'flex->name))
    (declare (ignorable __function__))
    (b* ((name (cond ((flexsum-p info) (flexsum->name info))
                     ((flexlist-p info)
                      (flexlist->name info))
                     ((flexalist-p info)
                      (flexalist->name info))
                     ((flextranssum-p info)
                      (flextranssum->name info))
                     ((flexset-p info) (flexset->name info))
                     ((flexomap-p info)
                      (flexomap->name info))
                     (t (raise "Internal error: malformed type ~x0."
                               info))))
         ((unless (symbolp name))
          (raise "Internal error: malformed type name ~x0."
                 name)))
      name)))

Theorem: symbolp-of-flex->name

(defthm symbolp-of-flex->name
  (b* ((name (flex->name info)))
    (symbolp name))
  :rule-classes :rewrite)