		Search-engine friendly clone of the ACL2 documentation.

Fgl-rewrite-rules

Lhses->branch-function-syms

Signature
(lhses->branch-function-syms lhses) → *
Arguments: lhses — Guard (pseudo-term-listp lhses).

Definitions and Theorems

Function: lhses->branch-function-syms

(defun lhses->branch-function-syms (lhses)
 (declare (xargs :guard (pseudo-term-listp lhses)))
 (let ((__function__ 'lhses->branch-function-syms))
  (declare (ignorable __function__))
  (b* (((when (atom lhses)) nil)
       (lhs (car lhses)))
   (pseudo-term-case
    lhs :fncall
    (if
     (and (eq lhs.fn 'if)
          (eql (len lhs.args) 3))
     (b* ((arg2 (second lhs.args)))
      (pseudo-term-case
           arg2
           :fncall
           (add-to-set-eq arg2.fn
                          (lhses->branch-function-syms (cdr lhses)))
           :otherwise (lhses->branch-function-syms (cdr lhses))))
     (lhses->branch-function-syms (cdr lhses)))
    :otherwise (lhses->branch-function-syms (cdr lhses))))))