		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.