		Search-engine friendly clone of the ACL2 documentation.

Tyname

Make-tyname

Basic constructor macro for tyname structures.

Syntax

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

Function: tyname

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