		Search-engine friendly clone of the ACL2 documentation.

Function-specifier

Function-specifier-kind

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

Signature
(function-specifier-kind x) → kind
Arguments: x — Guard (function-specifierp x).

Definitions and Theorems

Function: function-specifier-kind$inline

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

Theorem: function-specifier-kind-possibilities

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