		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Syntactically-zero-p

Signature
(syntactically-zero-p x) → result
Arguments: x — Guard (true-listp x).
Returns: result — Type (booleanp result).

Definitions and Theorems

Function: syntactically-zero-p

(defun syntactically-zero-p (x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'syntactically-zero-p))
    (declare (ignorable __function__))
    (b* (((mv head tail end) (first/rest/end x)))
      (and (eq head nil)
           (or end (syntactically-zero-p tail))))))

Theorem: booleanp-of-syntactically-zero-p

(defthm booleanp-of-syntactically-zero-p
  (b* ((result (syntactically-zero-p x)))
    (booleanp result))
  :rule-classes :rewrite)

Theorem: syntactically-zero-p-implies

(defthm syntactically-zero-p-implies
  (b* nil
    (implies (syntactically-zero-p x)
             (equal (bfr-list->s x env) 0))))