Turn a list of strings into a set of file paths.
(read-files-strings-to-paths strings) → paths
Function:
(defun read-files-strings-to-paths (strings) (declare (xargs :guard (string-listp strings))) (let ((__function__ 'read-files-strings-to-paths)) (declare (ignorable __function__)) (cond ((endp strings) nil) (t (insert (filepath (car strings)) (read-files-strings-to-paths (cdr strings)))))))
Theorem:
(defthm filepath-setp-of-read-files-strings-to-paths (b* ((paths (read-files-strings-to-paths strings))) (filepath-setp paths)) :rule-classes :rewrite)