		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.