		Search-engine friendly clone of the ACL2 documentation.

Function-definer

Function-definer-kind

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

Signature
(function-definer-kind x) → kind
Arguments: x — Guard (function-definerp x).

Definitions and Theorems

Function: function-definer-kind$inline

(defun function-definer-kind$inline (x)
  (declare (xargs :guard (function-definerp x)))
  (let ((__function__ 'function-definer-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :regular))
                       :regular)
                      (t :quantified))
         :exec (car x))))

Theorem: function-definer-kind-possibilities

(defthm function-definer-kind-possibilities
  (or (equal (function-definer-kind x)
             :regular)
      (equal (function-definer-kind x)
             :quantified))
  :rule-classes
  ((:forward-chaining :trigger-terms ((function-definer-kind x)))))