		Search-engine friendly clone of the ACL2 documentation.

Aig2c

Aig2c-main-list

Create the assignments for a list of AIGs.

Signature
(aig2c-main-list x seen tempmap config code) → (mv new-code seen)
Arguments: x — The AIG list to compile.; tempmap — Guard (string-listp (alist-vals tempmap)).; config — Guard (aig2c-config-p config).; code — Guard (character-listp code).
Returns: new-code — Type (character-listp new-code), given (force (character-listp code)).

Definitions and Theorems

Function: aig2c-main-list

(defun aig2c-main-list (x seen tempmap config code)
  (declare (xargs :guard (and (string-listp (alist-vals tempmap))
                              (aig2c-config-p config)
                              (character-listp code))))
  (let ((__function__ 'aig2c-main-list))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv code seen))
         ((mv code seen)
          (aig2c-main (car x)
                      seen tempmap config code)))
      (aig2c-main-list (cdr x)
                       seen tempmap config code))))

Theorem: character-listp-of-aig2c-main-list.new-code

(defthm character-listp-of-aig2c-main-list.new-code
  (implies (force (character-listp code))
           (b* (((mv ?new-code ?seen)
                 (aig2c-main-list x seen tempmap config code)))
             (character-listp new-code)))
  :rule-classes :rewrite)