		Search-engine friendly clone of the ACL2 documentation.

Meta-functions

Formal-true-listp

The definition of true-listp on formal terms.

Note that FORMAL-TRUE-LISTP is a `formal' predicate returning (QUOTE T) or (QUOTE NIL).

Definitions and Theorems

Function: formal-true-listp

(defun formal-true-listp (term)
  (declare (xargs :guard (pseudo-termp term)))
  (case-match term
    (('quote x)
     (cons 'quote
           (cons (true-listp x) 'nil)))
    (('cons x y)
     (declare (ignore x))
     (formal-true-listp y))
    (& *nil*)))