		Search-engine friendly clone of the ACL2 documentation.

Header-name-angles

Make-header-name-angles

Basic constructor macro for header-name-angles structures.

Syntax

(make-header-name-angles [:chars <chars>])

This is the usual way to construct header-name-angles structures. It simply conses together a structure with the specified fields.

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

Definition

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

Macro: make-header-name-angles

(defmacro make-header-name-angles (&rest args)
  (std::make-aggregate 'header-name-angles
                       args '((:chars))
                       'make-header-name-angles
                       nil))

Function: header-name-angles

(defun header-name-angles (chars)
  (declare (xargs :guard (h-char-listp chars)))
  (declare (xargs :guard t))
  (b* ((chars (mbe :logic (h-char-list-fix chars)
                   :exec chars)))
    (cons :angles chars)))