• 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-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-list

(faig-fix-list x) fixes every element of a list with faig-fix.

Signature

(faig-fix-list x) → *

Definitions and Theorems

Function: faig-fix-list

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