		Search-engine friendly clone of the ACL2 documentation.

Tyname

Make-tyname

Basic constructor macro for tyname structures.

Syntax

(make-tyname [:tyspec <tyspec>] 
             [:declor <declor>])

This is the usual way to construct tyname structures. It simply conses together a structure with the specified fields.

This macro generates a new tyname structure from scratch. See also change-tyname, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-tyname

(defmacro make-tyname (&rest args)
  (std::make-aggregate 'tyname
                       args '((:tyspec) (:declor))
                       'make-tyname
                       nil))

Function: tyname

(defun tyname (tyspec declor)
  (declare (xargs :guard (and (tyspecseqp tyspec)
                              (obj-adeclorp declor))))
  (declare (xargs :guard t))
  (let ((__function__ 'tyname))
    (declare (ignorable __function__))
    (b* ((tyspec (mbe :logic (tyspecseq-fix tyspec)
                      :exec tyspec))
         (declor (mbe :logic (obj-adeclor-fix declor)
                      :exec declor)))
      (cons :tyname (list (cons 'tyspec tyspec)
                          (cons 'declor declor))))))