		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

*-listp

Recognize true lists of *s.

Signature
(*-listp stars) → yes/no
Returns: yes/no — Type (booleanp yes/no).

These lists are used to indicate the number of arguments of function variables in defunvar.

Any * symbol (i.e. in any package) is allowed. Normally, the * in the current package should be used (without package qualifier), which is often the one from the main Lisp package, which other packages generally import.

Definitions and Theorems

Function: *-listp

(defun *-listp (stars)
  (declare (xargs :guard t))
  (let ((__function__ '*-listp))
    (declare (ignorable __function__))
    (if (atom stars)
        (null stars)
      (and (symbolp (car stars))
           (equal (symbol-name (car stars)) "*")
           (*-listp (cdr stars))))))

Theorem: booleanp-of-*-listp

(defthm booleanp-of-*-listp
  (b* ((yes/no (*-listp stars)))
    (booleanp yes/no))
  :rule-classes :rewrite)