		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Paths-add-scope

Signature
(paths-add-scope scope paths) → new-paths
Arguments: scope — Guard (name-p scope).; paths — Guard (pathlist-p paths).
Returns: new-paths — Type (pathlist-p new-paths).

Definitions and Theorems

Function: paths-add-scope

(defun paths-add-scope (scope paths)
  (declare (xargs :guard (and (name-p scope)
                              (pathlist-p paths))))
  (let ((__function__ 'paths-add-scope))
    (declare (ignorable __function__))
    (if (atom paths)
        nil
      (cons (make-path-scope :namespace scope
                             :subpath (car paths))
            (paths-add-scope scope (cdr paths))))))

Theorem: pathlist-p-of-paths-add-scope

(defthm pathlist-p-of-paths-add-scope
  (b* ((new-paths (paths-add-scope scope paths)))
    (pathlist-p new-paths))
  :rule-classes :rewrite)

Theorem: paths-add-scope-of-name-fix-scope

(defthm paths-add-scope-of-name-fix-scope
  (equal (paths-add-scope (name-fix scope) paths)
         (paths-add-scope scope paths)))

Theorem: paths-add-scope-name-equiv-congruence-on-scope

(defthm paths-add-scope-name-equiv-congruence-on-scope
  (implies (name-equiv scope scope-equiv)
           (equal (paths-add-scope scope paths)
                  (paths-add-scope scope-equiv paths)))
  :rule-classes :congruence)

Theorem: paths-add-scope-of-pathlist-fix-paths

(defthm paths-add-scope-of-pathlist-fix-paths
  (equal (paths-add-scope scope (pathlist-fix paths))
         (paths-add-scope scope paths)))

Theorem: paths-add-scope-pathlist-equiv-congruence-on-paths

(defthm paths-add-scope-pathlist-equiv-congruence-on-paths
  (implies (pathlist-equiv paths paths-equiv)
           (equal (paths-add-scope scope paths)
                  (paths-add-scope scope paths-equiv)))
  :rule-classes :congruence)