		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)