		Search-engine friendly clone of the ACL2 documentation.

Lhrange

Make-lhrange

Basic constructor macro for lhrange structures.

Syntax

(make-lhrange [:w <w>] 
              [:atom <atom>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-lhrange

(defmacro make-lhrange (&rest args)
  (std::make-aggregate 'lhrange
                       args '((:w) (:atom))
                       'make-lhrange
                       nil))

Function: lhrange

(defun lhrange (w atom)
  (declare (xargs :guard (and (posp w) (lhatom-p atom))))
  (declare (xargs :guard t))
  (let ((__function__ 'lhrange))
    (declare (ignorable __function__))
    (b* ((w (mbe :logic (pos-fix w) :exec w))
         (atom (mbe :logic (lhatom-fix atom)
                    :exec atom)))
      (if (eql w 1) atom (cons w atom)))))