		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Paths-to-vars

Extract variables from paths.

Signature
(paths-to-vars paths) → vars
Arguments: paths — Guard (path-listp paths).
Returns: vars — Type (identifier-list-resultp vars).

This lifts path-to-var to lists.

Definitions and Theorems

Function: paths-to-vars

(defun paths-to-vars (paths)
  (declare (xargs :guard (path-listp paths)))
  (let ((__function__ 'paths-to-vars))
    (declare (ignorable __function__))
    (b* (((when (endp paths)) nil)
         ((okf var) (path-to-var (car paths)))
         ((okf vars)
          (paths-to-vars (cdr paths))))
      (cons var vars))))

Theorem: identifier-list-resultp-of-paths-to-vars

(defthm identifier-list-resultp-of-paths-to-vars
  (b* ((vars (paths-to-vars paths)))
    (identifier-list-resultp vars))
  :rule-classes :rewrite)

Theorem: len-of-paths-to-vars

(defthm len-of-paths-to-vars
  (b* ((?vars (paths-to-vars paths)))
    (implies (not (reserrp vars))
             (equal (len vars) (len paths)))))

Theorem: error-info-wfp-of-paths-to-vars

(defthm error-info-wfp-of-paths-to-vars
  (b* ((?vars (paths-to-vars paths)))
    (implies (reserrp vars)
             (error-info-wfp vars))))

Theorem: paths-to-vars-of-path-list-fix-paths

(defthm paths-to-vars-of-path-list-fix-paths
  (equal (paths-to-vars (path-list-fix paths))
         (paths-to-vars paths)))

Theorem: paths-to-vars-path-list-equiv-congruence-on-paths

(defthm paths-to-vars-path-list-equiv-congruence-on-paths
  (implies (path-list-equiv paths paths-equiv)
           (equal (paths-to-vars paths)
                  (paths-to-vars paths-equiv)))
  :rule-classes :congruence)