		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-ctrex-ncols

Signature
(fraig-ctrex-ncols fraig-ctrexes) → ncols
Returns: ncols — Type (natp ncols).

Definitions and Theorems

Function: fraig-ctrex-ncols

(defun fraig-ctrex-ncols (fraig-ctrexes)
  (declare (xargs :stobjs (fraig-ctrexes)))
  (declare (xargs :guard t))
  (let ((__function__ 'fraig-ctrex-ncols))
    (declare (ignorable __function__))
    (b* (((acl2::stobj-get size)
          ((s32v (fraig-ctrex-data fraig-ctrexes)))
          (s32v-ncols s32v)))
      size)))

Theorem: natp-of-fraig-ctrex-ncols

(defthm natp-of-fraig-ctrex-ncols
  (b* ((ncols (fraig-ctrex-ncols fraig-ctrexes)))
    (natp ncols))
  :rule-classes :type-prescription)