		Search-engine friendly clone of the ACL2 documentation.

Position

Make-position

Basic constructor macro for position structures.

Syntax

(make-position [:line <line>] 
               [:column <column>])

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

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

Definition

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

Macro: make-position

(defmacro make-position (&rest args)
  (std::make-aggregate 'position
                       args '((:line) (:column))
                       'make-position
                       nil))

Function: position

(defun position (line column)
  (declare (xargs :guard (and (posp line) (natp column))))
  (declare (xargs :guard t))
  (let ((__function__ 'position))
    (declare (ignorable __function__))
    (b* ((line (mbe :logic (acl2::pos-fix line)
                    :exec line))
         (column (mbe :logic (nfix column)
                      :exec column)))
      (list (cons 'line line)
            (cons 'column column)))))