		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Toplevel-name

Signature
(toplevel-name top) → nm
Arguments: top — Guard (toplevelp top).
Returns: nm — Type (stringp nm).

Definitions and Theorems

Function: toplevel-name

(defun toplevel-name (top)
 (declare (xargs :guard (toplevelp top)))
 (let ((__function__ 'toplevel-name))
  (declare (ignorable __function__))
  (if
   (toplevelp top)
   (toplevel-case
    top :type
    (identifier->name (type-definition->name top.get))
    :types
    (let ((tys (type-recursion->definitions top.get)))
      (if (endp tys)
          ""
        (identifier->name (type-definition->name (car tys)))))
    :function
    (identifier->name
      (function-header->name (function-definition->header top.get)))
    :functions
    (let ((fns (function-recursion->definitions top.get)))
      (if (endp fns)
          ""
        (identifier->name
             (function-header->name
                  (function-definition->header (car fns))))))
    :specification
    (identifier->name (function-specification->name top.get))
    :theorem (identifier->name (theorem->name top.get))
    :transform
    (identifier->name (transform->new-function-name top.get)))
   "")))

Theorem: stringp-of-toplevel-name

(defthm stringp-of-toplevel-name
  (b* ((nm (toplevel-name top)))
    (stringp nm))
  :rule-classes :rewrite)