		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr-list-purep

Check if all the expressions in a list are pure.

Signature
(expr-list-purep x) → std::bool

This is an ordinary std::deflist. It is "loose" in that it does not care whether x is nil-terminated.

Definitions and Theorems

Function: expr-list-purep

(defun expr-list-purep (x)
  (declare (xargs :guard (expr-listp x)))
  (if (consp x)
      (and (expr-purep (car x))
           (expr-list-purep (cdr x)))
    t))

Subtopics

Expr-list-purep-basics: Basic theorems about expr-list-purep, generated by std::deflist.