		Search-engine friendly clone of the ACL2 documentation.

Natoption/natoptionlist

Natoption/natoptionlist-kind

Get the kind (tag) of a natoption/natoptionlist structure.

Signature
(natoption/natoptionlist-kind x) → kind
Arguments: x — Guard (natoption/natoptionlist-p x).

Definitions and Theorems

Function: natoption/natoptionlist-kind$inline

(defun natoption/natoptionlist-kind$inline (x)
  (declare (xargs :guard (natoption/natoptionlist-p x)))
  (let ((__function__ 'natoption/natoptionlist-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :one)) :one)
                      (t :list))
         :exec (car x))))

Theorem: natoption/natoptionlist-kind-possibilities

(defthm natoption/natoptionlist-kind-possibilities
  (or (equal (natoption/natoptionlist-kind x)
             :one)
      (equal (natoption/natoptionlist-kind x)
             :list))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((natoption/natoptionlist-kind x)))))