		Search-engine friendly clone of the ACL2 documentation.

The-true-list

Coerce an expected true list to a true list

Like true-list-fix, the-true-list logically returns its argument unchanged if that argument satisfies true-listp and otherwise returns a corresponding ``fixed'' true list. Unlike true-list-fix, the guard for (the-true-list x) is (true-listp x), and (the-true-list x) evaluates immediately to x in raw Lisp (see guards-and-evaluation for relevant discussion).

Function: the-true-list

(defun the-true-list (x)
  (declare (xargs :guard (true-listp x)))
  (mbe :logic (true-list-fix x) :exec x))