		Search-engine friendly clone of the ACL2 documentation.

Vl-string-between-locs

Vl-location-before-nofilename

Signature
(vl-location-before-nofilename x y) → *
Arguments: x — Guard (vl-location-p x).; y — Guard (vl-location-p y).

Definitions and Theorems

Function: vl-location-before-nofilename

(defun vl-location-before-nofilename (x y)
  (declare (xargs :guard (and (vl-location-p x)
                              (vl-location-p y))))
  (let ((__function__ 'vl-location-before-nofilename))
    (declare (ignorable __function__))
    (b* (((vl-location x) x)
         ((vl-location y) y))
      (or (< x.line y.line)
          (and (eql x.line y.line)
               (< x.col y.col))))))