		Search-engine friendly clone of the ACL2 documentation.

Faig

Faig-compose-alist

(faig-compose-alist x sigma) composes into an FAIG Alist (an alist binding keys to FAIGs).

Signature
(faig-compose-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-compose-alist

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

Subtopics

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