		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

Fgl::fgl-list-object-bfrcounts

Signature
(fgl::fgl-list-object-bfrcounts x) → fgl::counts
Arguments: x — Guard (fgl::fgl-object-p x).
Returns: fgl::counts — Type (nat-listp fgl::counts).

Definitions and Theorems

Function: fgl-list-object-bfrcounts

(defun fgl::fgl-list-object-bfrcounts (x)
  (declare (xargs :guard (fgl::fgl-object-p x)))
  (let ((__function__ 'fgl::fgl-list-object-bfrcounts))
    (declare (ignorable __function__))
    (fgl::fgl-object-case
         x
         :g-concrete (repeat (len fgl::x.val) 0)
         :g-cons (cons (fgl::fgl-object-bfrcount fgl::x.car)
                       (fgl::fgl-list-object-bfrcounts fgl::x.cdr))
         :otherwise nil)))

Theorem: nat-listp-of-fgl-list-object-bfrcounts

(defthm fgl::nat-listp-of-fgl-list-object-bfrcounts
  (b* ((fgl::counts (fgl::fgl-list-object-bfrcounts x)))
    (nat-listp fgl::counts))
  :rule-classes :rewrite)