		Search-engine friendly clone of the ACL2 documentation.

Smt-hint-interface

True-list-fix

Fixing function for true-listp.

Signature
(true-list-fix lst) → fixed-lst
Arguments: lst — Guard (true-listp lst).
Returns: fixed-lst — Type (true-listp fixed-lst).

Definitions and Theorems

Function: true-list-fix

(defun true-list-fix (lst)
  (declare (xargs :guard (true-listp lst)))
  (let ((acl2::__function__ 'true-list-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (consp lst)
             (cons (car lst)
                   (true-list-fix (cdr lst)))
           nil)
         :exec lst)))

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

(defthm true-listp-of-true-list-fix
  (b* ((fixed-lst (true-list-fix lst)))
    (true-listp fixed-lst))
  :rule-classes :rewrite)