		Search-engine friendly clone of the ACL2 documentation.

Oslib

Catpaths

Extend a base directory with many file names.

Signature
(catpaths basedir filenames) → paths
Arguments: basedir — Directory whose name should be extended, which may or may not end with a slash.
Guard (stringp basedir).; filenames — Names of files to append to basedir.
Guard (string-listp filenames).
Returns: paths — Extended paths.
Type (string-listp paths).

Definitions and Theorems

Function: catpaths

(defun catpaths (basedir filenames)
  (declare (xargs :guard (and (stringp basedir)
                              (string-listp filenames))))
  (let ((__function__ 'catpaths))
    (declare (ignorable __function__))
    (if (atom filenames)
        nil
      (cons (catpath basedir (car filenames))
            (catpaths basedir (cdr filenames))))))

Theorem: string-listp-of-catpaths

(defthm string-listp-of-catpaths
  (b* ((paths (catpaths basedir filenames)))
    (string-listp paths))
  :rule-classes :rewrite)