		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Names->paths

Signature
(names->paths names) → new-paths
Arguments: names — Guard (namelist-p names).
Returns: new-paths — Type (pathlist-p new-paths).

Definitions and Theorems

Function: names->paths

(defun names->paths (names)
  (declare (xargs :guard (namelist-p names)))
  (let ((__function__ 'names->paths))
    (declare (ignorable __function__))
    (if (atom names)
        nil
      (cons (make-path-wire :name (car names))
            (names->paths (cdr names))))))

Theorem: pathlist-p-of-names->paths

(defthm pathlist-p-of-names->paths
  (b* ((new-paths (names->paths names)))
    (pathlist-p new-paths))
  :rule-classes :rewrite)

Theorem: names->paths-of-namelist-fix-names

(defthm names->paths-of-namelist-fix-names
  (equal (names->paths (namelist-fix names))
         (names->paths names)))

Theorem: names->paths-namelist-equiv-congruence-on-names

(defthm names->paths-namelist-equiv-congruence-on-names
  (implies (namelist-equiv names names-equiv)
           (equal (names->paths names)
                  (names->paths names-equiv)))
  :rule-classes :congruence)