		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

If-tree-leaf-terms

Collect the leaf terms according to the if tree structure of a term.

Signature
(if-tree-leaf-terms term) → leaf-terms
Arguments: term — Guard (pseudo-termp term).
Returns: leaf-terms — Type (pseudo-term-listp leaf-terms), given the guard.

If term is not a call of if, we return the singleton list with term as the only leaf.

If term has the form (if a b c), we recursively collect the leaves of b of c, and join them into a list.

Definitions and Theorems

Function: if-tree-leaf-terms

(defun if-tree-leaf-terms (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'if-tree-leaf-terms))
    (declare (ignorable __function__))
    (cond ((variablep term) (list term))
          ((fquotep term) (list term))
          ((eq (ffn-symb term) 'if)
           (append (if-tree-leaf-terms (fargn term 2))
                   (if-tree-leaf-terms (fargn term 3))))
          (t (list term)))))

Theorem: pseudo-term-listp-of-if-tree-leaf-terms

(defthm pseudo-term-listp-of-if-tree-leaf-terms
  (implies (and (pseudo-termp term))
           (b* ((leaf-terms (if-tree-leaf-terms term)))
             (pseudo-term-listp leaf-terms)))
  :rule-classes :rewrite)