		Search-engine friendly clone of the ACL2 documentation.

Translated-terms

Tterm-case-constant-listp

Lift (tterm-case ... :constant) to lists.

Signature
(tterm-case-constant-listp x) → std::bool

This checks if all the terms in a list are quoted constants.

Definitions and Theorems

Function: tterm-case-constant-listp

(defun tterm-case-constant-listp (x)
  (declare (xargs :guard (tterm-listp x)))
  (let ((__function__ 'tterm-case-constant-listp))
    (declare (ignorable __function__))
    (if (consp x)
        (and (tterm-case (car x) :constant)
             (tterm-case-constant-listp (cdr x)))
      (null x))))

Subtopics

Tterm-case-constant-listp-basics: Basic theorems about tterm-case-constant-listp, generated by std::deflist.