		Search-engine friendly clone of the ACL2 documentation.

Location-tuple-comp

Make-location-tuple-comp

Basic constructor macro for location-tuple-comp structures.

Syntax

(make-location-tuple-comp [:tuple <tuple>] 
                          [:index <index>])

This is the usual way to construct location-tuple-comp structures. It simply conses together a structure with the specified fields.

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

Definition

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

Macro: make-location-tuple-comp

(defmacro make-location-tuple-comp (&rest args)
  (std::make-aggregate 'location-tuple-comp
                       args '((:tuple) (:index))
                       'make-location-tuple-comp
                       nil))

Function: location-tuple-comp

(defun location-tuple-comp (tuple index)
  (declare (xargs :guard (and (locationp tuple) (natp index))))
  (declare (xargs :guard t))
  (let ((__function__ 'location-tuple-comp))
    (declare (ignorable __function__))
    (b* ((tuple (mbe :logic (location-fix tuple)
                     :exec tuple))
         (index (mbe :logic (nfix index) :exec index)))
      (cons :tuple-comp (list tuple index)))))