		Search-engine friendly clone of the ACL2 documentation.

4v->faig-const

4v-list->faig-const-list

Signature
(4v-list->faig-const-list x) → *

Definitions and Theorems

Function: 4v-list->faig-const-list

(defun 4v-list->faig-const-list (x)
  (declare (xargs :guard t))
  (let ((__function__ '4v-list->faig-const-list))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (4v->faig-const (car x))
            (4v-list->faig-const-list (cdr x))))))

Theorem: nth-of-4v-list->faig-const-list

(defthm nth-of-4v-list->faig-const-list
  (faig-const-equiv (nth n (4v-list->faig-const-list x))
                    (4v->faig-const (nth n x))))