		Search-engine friendly clone of the ACL2 documentation.

Ternary-op

Ternary-op-kind

Get the kind (tag) of a ternary-op structure.

Signature
(ternary-op-kind x) → kind
Arguments: x — Guard (ternary-opp x).

Definitions and Theorems

Function: ternary-op-kind$inline

(defun ternary-op-kind$inline (x)
  (declare (xargs :guard (ternary-opp x)))
  (let ((__function__ 'ternary-op-kind))
    (declare (ignorable __function__))
    (mbe :logic (case (tag x) (otherwise :ternary))
         :exec (car x))))

Theorem: ternary-op-kind-possibilities

(defthm ternary-op-kind-possibilities
  (or (equal (ternary-op-kind x) :ternary))
  :rule-classes
  ((:forward-chaining :trigger-terms ((ternary-op-kind x)))))