`(vl-location-between-p x min max)` is true exactly when

- Signature
(vl-location-between-p x min max) → *

- Arguments
`x`—Guard (vl-location-p x) .`min`—Guard (vl-location-p min) .`max`—Guard (vl-location-p max) .

**Function: **

(defun vl-location-between-p (x min max) (declare (xargs :guard (and (vl-location-p x) (vl-location-p min) (vl-location-p max)))) (let ((__function__ 'vl-location-between-p)) (declare (ignorable __function__)) (b* (((vl-location x) x) ((vl-location low) min) ((vl-location high) max)) (and (equal x.filename low.filename) (equal x.filename high.filename) (or (< low.line x.line) (and (eql low.line x.line) (<= low.col x.col))) (or (< x.line high.line) (and (eql x.line high.line) (<= x.col high.col)))))))

**Theorem: **

(defthm vl-location-between-p-of-vl-location-fix-x (equal (vl-location-between-p (vl-location-fix x) min max) (vl-location-between-p x min max)))

**Theorem: **

(defthm vl-location-between-p-vl-location-equiv-congruence-on-x (implies (vl-location-equiv x x-equiv) (equal (vl-location-between-p x min max) (vl-location-between-p x-equiv min max))) :rule-classes :congruence)

**Theorem: **

(defthm vl-location-between-p-of-vl-location-fix-min (equal (vl-location-between-p x (vl-location-fix min) max) (vl-location-between-p x min max)))

**Theorem: **

(defthm vl-location-between-p-vl-location-equiv-congruence-on-min (implies (vl-location-equiv min min-equiv) (equal (vl-location-between-p x min max) (vl-location-between-p x min-equiv max))) :rule-classes :congruence)

**Theorem: **

(defthm vl-location-between-p-of-vl-location-fix-max (equal (vl-location-between-p x min (vl-location-fix max)) (vl-location-between-p x min max)))

**Theorem: **

(defthm vl-location-between-p-vl-location-equiv-congruence-on-max (implies (vl-location-equiv max max-equiv) (equal (vl-location-between-p x min max) (vl-location-between-p x min max-equiv))) :rule-classes :congruence)