		Search-engine friendly clone of the ACL2 documentation.

Token+span

Make-token+span

Basic constructor macro for token+span structures.

Syntax

(make-token+span [:token <token>] 
                 [:span <span>])

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

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

Definition

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

Macro: make-token+span

(defmacro make-token+span (&rest args)
  (std::make-aggregate 'token+span
                       args '((:token) (:span))
                       'make-token+span
                       nil))

Function: token+span

(defun token+span (token span)
  (declare (xargs :guard (and (tokenp token) (spanp span))))
  (declare (xargs :guard t))
  (let ((__function__ 'token+span))
    (declare (ignorable __function__))
    (b* ((token (mbe :logic (token-fix token)
                     :exec token))
         (span (mbe :logic (span-fix span)
                    :exec span)))
      (list (cons 'token token)
            (cons 'span span)))))