		Search-engine friendly clone of the ACL2 documentation.

Tyname

Make-tyname

Basic constructor macro for tyname structures.

Syntax

(make-tyname [:specqual <specqual>] 
             [:decl? <decl?>])

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 '((:specqual) (:decl?))
                       'make-tyname
                       nil))

Function: tyname

(defun tyname (specqual decl?)
  (declare (xargs :guard (and (spec/qual-listp specqual)
                              (absdeclor-optionp decl?))))
  (declare (xargs :guard t))
  (let ((__function__ 'tyname))
    (declare (ignorable __function__))
    (b* ((specqual (mbe :logic (spec/qual-list-fix specqual)
                        :exec specqual))
         (decl? (mbe :logic (absdeclor-option-fix decl?)
                     :exec decl?)))
      (list (cons 'specqual specqual)
            (cons 'decl? decl?)))))