		Search-engine friendly clone of the ACL2 documentation.

Faig-restrict

Faig-restrict-alist

(faig-restrict-alist x sigma) substitutes into an FAIG alist (an alist binding keys to FAIGs).

Signature
(faig-restrict-alist x sigma) → *

The alist x does not need to be fast, and we produce an ordinary (slow) alist as a result.

Definitions and Theorems

Function: faig-restrict-alist

(defun faig-restrict-alist (x sigma)
       (declare (xargs :guard t))
       (let ((__function__ 'faig-restrict-alist))
            (declare (ignorable __function__))
            (b* (((when (atom x)) nil)
                 (rest (faig-restrict-alist (cdr x) sigma))
                 ((when (atom (car x))) rest))
                (cons (cons (caar x)
                            (faig-restrict (cdar x) sigma))
                      rest))))

Subtopics

Faig-restrict-alist-thms: Basic theorems about faig-restrict-alist.