		Search-engine friendly clone of the ACL2 documentation.

Vl-find-file

Vl-ends-with-directory-separatorp

Signature
(vl-ends-with-directory-separatorp x) → bool
Arguments: x — Guard (stringp x).
Returns: bool — Type (booleanp bool).

Definitions and Theorems

Function: vl-ends-with-directory-separatorp

(defun vl-ends-with-directory-separatorp (x)
  (declare (xargs :guard (stringp x)))
  (let ((__function__ 'vl-ends-with-directory-separatorp))
    (declare (ignorable __function__))
    (let ((x (string-fix x)) (len (length x)))
      (and (/= len 0)
           (eql (char x (- (length x) 1))
                acl2::*directory-separator*)))))

Theorem: booleanp-of-vl-ends-with-directory-separatorp

(defthm booleanp-of-vl-ends-with-directory-separatorp
  (b* ((bool (vl-ends-with-directory-separatorp x)))
    (booleanp bool))
  :rule-classes :type-prescription)

Theorem: vl-ends-with-directory-separatorp-of-str-fix-x

(defthm vl-ends-with-directory-separatorp-of-str-fix-x
  (equal (vl-ends-with-directory-separatorp (str-fix x))
         (vl-ends-with-directory-separatorp x)))

Theorem: vl-ends-with-directory-separatorp-streqv-congruence-on-x

(defthm vl-ends-with-directory-separatorp-streqv-congruence-on-x
  (implies (streqv x x-equiv)
           (equal (vl-ends-with-directory-separatorp x)
                  (vl-ends-with-directory-separatorp x-equiv)))
  :rule-classes :congruence)