		Search-engine friendly clone of the ACL2 documentation.

Function-denv-option

Function-denv-option-kind

Get the kind (tag) of a function-denv-option structure.

Signature
(function-denv-option-kind x) → kind
Arguments: x — Guard (function-denv-optionp x).

Definitions and Theorems

Function: function-denv-option-kind$inline

(defun function-denv-option-kind$inline (x)
  (declare (xargs :guard (function-denv-optionp x)))
  (let ((__function__ 'function-denv-option-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :some)) :some)
                      (t :none))
         :exec (car x))))

Theorem: function-denv-option-kind-possibilities

(defthm function-denv-option-kind-possibilities
  (or (equal (function-denv-option-kind x)
             :some)
      (equal (function-denv-option-kind x)
             :none))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((function-denv-option-kind x)))))