		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-ctrex-in/reg-rows

Signature
(fraig-ctrex-in/reg-rows fraig-ctrexes) → *

Definitions and Theorems

Function: fraig-ctrex-in/reg-rows

(defun fraig-ctrex-in/reg-rows (fraig-ctrexes)
  (declare (xargs :stobjs (fraig-ctrexes)))
  (declare (xargs :guard t))
  (let ((__function__ 'fraig-ctrex-in/reg-rows))
    (declare (ignorable __function__))
    (b* (((acl2::stobj-get size)
          ((s32v (fraig-ctrex-in/reg-relevants fraig-ctrexes)))
          (s32v-nrows s32v)))
      size)))