• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
        • Faig-constructors
        • Faig-onoff-equiv
        • Faig-purebool-p
        • Faig-alist-equiv
        • Faig-equiv
        • Faig-eval
        • Faig-restrict
        • Faig-fix
          • Faig-fix-alist
            • Faig-fix-alist-thms
          • Faig-fix-thms
          • Faig-fix-list
        • Faig-partial-eval
        • Faig-compose
        • Faig-compose-alist
        • Patbind-faig
        • Faig-constants
      • Bed
      • 4v
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Faig-fix

Faig-fix-alist

(faig-fix-alist x) fixes every value in an alist with faig-fix.

Signature
(faig-fix-alist x) → *

Definitions and Theorems

Function: faig-fix-alist

(defun faig-fix-alist (x)
  (declare (xargs :guard t))
  (let ((__function__ 'faig-fix-alist))
    (declare (ignorable __function__))
    (cond ((atom x) nil)
          ((atom (car x))
           (faig-fix-alist (cdr x)))
          (t (cons (cons (caar x) (faig-fix (cdar x)))
                   (faig-fix-alist (cdr x)))))))

Subtopics

Faig-fix-alist-thms
Basic theorems about faig-fix-alist.