• Top

• Vl-portinfo-regular

Vl-portinfo-regular->interfacep

Get the interfacep field from a vl-portinfo-regular.

Signature

(vl-portinfo-regular->interfacep x) → interfacep

Arguments

x — Guard (vl-portinfo-p x).

Returns

interfacep — Type (booleanp interfacep).

This is an ordinary field accessor created by defprod.

Definitions and Theorems

Function: vl-portinfo-regular->interfacep$inline

(defun vl-portinfo-regular->interfacep$inline (x)
 (declare (xargs :guard (vl-portinfo-p x)))
 (declare (xargs :guard (equal (vl-portinfo-kind x) :regular)))
 (let ((__function__ 'vl-portinfo-regular->interfacep))
  (declare (ignorable __function__))
  (mbe
    :logic
    (b* ((x (and (equal (vl-portinfo-kind x) :regular)
                 x)))
      (acl2::bool-fix
           (std::prod-cdr (std::prod-cdr (std::prod-cdr (cdr x))))))
    :exec (std::prod-cdr (std::prod-cdr (std::prod-cdr (cdr x)))))))

Theorem: booleanp-of-vl-portinfo-regular->interfacep

(defthm booleanp-of-vl-portinfo-regular->interfacep
  (b* ((interfacep (vl-portinfo-regular->interfacep$inline x)))
    (booleanp interfacep))
  :rule-classes :rewrite)

Theorem: vl-portinfo-regular->interfacep$inline-of-vl-portinfo-fix-x

(defthm vl-portinfo-regular->interfacep$inline-of-vl-portinfo-fix-x
 (equal (vl-portinfo-regular->interfacep$inline (vl-portinfo-fix x))
        (vl-portinfo-regular->interfacep$inline x)))

Theorem: vl-portinfo-regular->interfacep$inline-vl-portinfo-equiv-congruence-on-x

(defthm
 vl-portinfo-regular->interfacep$inline-vl-portinfo-equiv-congruence-on-x
 (implies (vl-portinfo-equiv x x-equiv)
          (equal (vl-portinfo-regular->interfacep$inline x)
                 (vl-portinfo-regular->interfacep$inline x-equiv)))
 :rule-classes :congruence)

Theorem: vl-portinfo-regular->interfacep-when-wrong-kind

(defthm vl-portinfo-regular->interfacep-when-wrong-kind
  (implies (not (equal (vl-portinfo-kind x) :regular))
           (equal (vl-portinfo-regular->interfacep x)
                  (acl2::bool-fix nil))))