		Search-engine friendly clone of the ACL2 documentation.

Vl-port

Vl-port-p

Recognizer for vl-port.

Signature
(vl-port-p x) → *

Definitions and Theorems

Function: vl-port-p

(defun vl-port-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-port-p))
    (declare (ignorable __function__))
    (common-lisp::case (tag x)
      ((:vl-regularport) (vl-regularport-p x))
      (otherwise (vl-interfaceport-p x)))))

Theorem: consp-when-vl-port-p

(defthm consp-when-vl-port-p
  (implies (vl-port-p x) (consp x))
  :rule-classes :compound-recognizer)

Theorem: vl-port-p-when-vl-regularport-p

(defthm vl-port-p-when-vl-regularport-p
  (implies (vl-regularport-p x)
           (vl-port-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-port-p-when-vl-interfaceport-p

(defthm vl-port-p-when-vl-interfaceport-p
  (implies (vl-interfaceport-p x)
           (vl-port-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-regularport-p-by-tag-when-vl-port-p

(defthm vl-regularport-p-by-tag-when-vl-port-p
  (implies (and (or (equal (tag x) :vl-regularport))
                (vl-port-p x))
           (vl-regularport-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-interfaceport-p-by-tag-when-vl-port-p

(defthm vl-interfaceport-p-by-tag-when-vl-port-p
  (implies (and (or (equal (tag x) :vl-interfaceport))
                (vl-port-p x))
           (vl-interfaceport-p x))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: vl-port-p-when-invalid-tag

(defthm vl-port-p-when-invalid-tag
  (implies (and (not (equal (tag x) :vl-regularport))
                (not (equal (tag x) :vl-interfaceport)))
           (not (vl-port-p x)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: tag-when-vl-port-p-forward

(defthm tag-when-vl-port-p-forward
  (implies (vl-port-p x)
           (or (equal (tag x) :vl-regularport)
               (equal (tag x) :vl-interfaceport)))
  :rule-classes ((:forward-chaining)))

Subtopics

Port-tools: Basic functions for working with arguments and ports.