		Search-engine friendly clone of the ACL2 documentation.

List-fix

(list-fix x) converts x into a true-listp by, if necessary, changing its final-cdr to nil.

list-fix is really a macro which expands to a call to true-list-fix with the same argument.

See also llist-fix, a "logical list fix" that is guarded with true-listp for greater efficiency.

Macro: list-fix-exec

(defmacro list-fix-exec (x)
  (cons 'true-list-fix-exec
        (cons x 'nil)))

Macro: list-fix

(defmacro list-fix (x)
  (cons 'true-list-fix (cons x 'nil)))

Definitions and Theorems

Theorem: list-fix-when-not-consp

(defthm list-fix-when-not-consp
  (implies (not (consp x))
           (equal (list-fix x) nil)))

Theorem: list-fix-of-cons

(defthm list-fix-of-cons
  (equal (list-fix (cons a x))
         (cons a (list-fix x))))

Theorem: list-fix-exec-removal

(defthm list-fix-exec-removal
  (equal (list-fix-exec x) (list-fix x)))

Theorem: car-of-list-fix

(defthm car-of-list-fix
  (equal (car (list-fix x)) (car x)))

Theorem: cdr-of-list-fix

(defthm cdr-of-list-fix
  (equal (cdr (list-fix x))
         (list-fix (cdr x))))

Theorem: list-fix-when-len-zero

(defthm list-fix-when-len-zero
  (implies (equal (len x) 0)
           (equal (list-fix x) nil)))

Theorem: true-listp-of-list-fix

(defthm true-listp-of-list-fix
  (true-listp (list-fix x)))

Theorem: len-of-list-fix

(defthm len-of-list-fix
  (equal (len (list-fix x)) (len x)))

Theorem: list-fix-when-true-listp

(defthm list-fix-when-true-listp
  (implies (true-listp x)
           (equal (list-fix x) x)))

Theorem: list-fix-under-iff

(defthm list-fix-under-iff
  (iff (list-fix x) (consp x)))

Theorem: consp-of-list-fix

(defthm consp-of-list-fix
  (equal (consp (list-fix x)) (consp x)))

Theorem: last-of-list-fix

(defthm last-of-list-fix
  (equal (last (list-fix x))
         (list-fix (last x))))

Theorem: equal-of-list-fix-and-self

(defthm equal-of-list-fix-and-self
  (equal (equal x (list-fix x))
         (true-listp x)))

Theorem: element-list-p-of-list-fix-non-true-listp

(defthm element-list-p-of-list-fix-non-true-listp
  (implies (element-list-final-cdr-p t)
           (equal (element-list-p (list-fix x))
                  (element-list-p x)))
  :rule-classes :rewrite)

Theorem: element-list-p-of-list-fix-true-listp

(defthm element-list-p-of-list-fix-true-listp
  (implies (element-list-p x)
           (element-list-p (list-fix x)))
  :rule-classes :rewrite)

Theorem: element-list-fix-of-list-fix-true-list

(defthm element-list-fix-of-list-fix-true-list
  (implies (not (element-list-final-cdr-p t))
           (equal (element-list-fix (list-fix x))
                  (element-list-fix x)))
  :rule-classes :rewrite)

Theorem: element-list-fix-of-list-fix-non-true-list

(defthm element-list-fix-of-list-fix-non-true-list
  (implies (element-list-final-cdr-p t)
           (equal (element-list-fix (list-fix x))
                  (list-fix (element-list-fix x))))
  :rule-classes :rewrite)

Theorem: elementlist-projection-of-list-fix

(defthm elementlist-projection-of-list-fix
  (equal (elementlist-projection (list-fix x))
         (elementlist-projection x))
  :rule-classes :rewrite)

Theorem: elementlist-mapappend-of-list-fix

(defthm elementlist-mapappend-of-list-fix
  (equal (elementlist-mapappend (list-fix x))
         (elementlist-mapappend x))
  :rule-classes :rewrite)

Subtopics

Llist-fix: (llist-fix x) is locally just list-fix, but it is guarded with true-listp so that in the execution it is just an identity function.