		Search-engine friendly clone of the ACL2 documentation.

Vl-find-file

Vl-extend-pathname

(vl-extend-pathname dir filename) concatenates dir and filename, adding a slash to between them only if dir does not end with a slash.

Definitions and Theorems

Function: vl-ends-with-directory-separatorp

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

Function: vl-extend-pathname

(defun vl-extend-pathname (dir filename)
  (declare (xargs :guard (and (stringp dir) (stringp filename))))
  (cat dir
       (if (vl-ends-with-directory-separatorp dir)
           ""
         (implode (list acl2::*directory-separator*)))
       filename))

Theorem: stringp-of-vl-extend-pathname

(defthm stringp-of-vl-extend-pathname
  (stringp (vl-extend-pathname dir filename))
  :rule-classes :type-prescription)