		Search-engine friendly clone of the ACL2 documentation.

Vl-propbinary

Vl-property-binaryop-p

Very basic binary sequence/property operators.

The only confusing thing here is the different kinds of implies and follows operators. Here's the mapping:

:vl-prop-word-implies is literally the keyword implies.
:vl-prop-thin-implies is the operator |->, i.e., overlapped implication.
:vl-prop-fat-implies is the operator |=>, i.e., non-overlapped implication.
:vl-prop-thin-follows is the operator #-#.
:vl-prop-fat-follows is the operator #=#.

This is an ordinary defenum.

Function: vl-property-binaryop-p

(defun vl-property-binaryop-p (x)
  (declare (xargs :guard t))
  (or (eq x ':vl-prop-and)
      (eq x ':vl-prop-intersect)
      (eq x ':vl-prop-or)
      (eq x ':vl-prop-within)
      (eq x ':vl-prop-iff)
      (eq x ':vl-prop-until)
      (eq x ':vl-prop-suntil)
      (eq x ':vl-prop-untilwith)
      (eq x ':vl-prop-suntilwith)
      (eq x ':vl-prop-word-implies)
      (eq x ':vl-prop-thin-implies)
      (eq x ':vl-prop-fat-implies)
      (eq x ':vl-prop-thin-follows)
      (eq x ':vl-prop-fat-follows)))

Theorem: type-when-vl-property-binaryop-p

(defthm type-when-vl-property-binaryop-p
  (implies (vl-property-binaryop-p x)
           (if (symbolp x)
               (if (not (equal x 't))
                   (not (equal x 'nil))
                 'nil)
             'nil))
  :rule-classes :compound-recognizer)

Subtopics

Vl-property-binaryop->string