		Search-engine friendly clone of the ACL2 documentation.

Fgl-object

Fgl-object-kind

Get the kind (tag) of a fgl-object structure.

Signature
(fgl-object-kind x) → kind
Arguments: x — Guard (fgl-object-p x).

Definitions and Theorems

Function: fgl-object-kind$inline

(defun fgl-object-kind$inline (x)
  (declare (xargs :guard (fgl-object-p x)))
  (let ((__function__ 'fgl-object-kind))
    (declare (ignorable __function__))
    (cond ((or (atom x) (eq (car x) :g-concrete))
           :g-concrete)
          ((eq (car x) :g-boolean) :g-boolean)
          ((eq (car x) :g-integer) :g-integer)
          ((eq (car x) :g-ite) :g-ite)
          ((eq (car x) :g-apply) :g-apply)
          ((eq (car x) :g-var) :g-var)
          ((and (consp (car x))
                (eq (caar x) :g-map))
           :g-map)
          (t :g-cons))))

Theorem: fgl-object-kind-possibilities

(defthm fgl-object-kind-possibilities
  (or (equal (fgl-object-kind x) :g-concrete)
      (equal (fgl-object-kind x) :g-boolean)
      (equal (fgl-object-kind x) :g-integer)
      (equal (fgl-object-kind x) :g-ite)
      (equal (fgl-object-kind x) :g-apply)
      (equal (fgl-object-kind x) :g-var)
      (equal (fgl-object-kind x) :g-map)
      (equal (fgl-object-kind x) :g-cons))
  :rule-classes
  ((:forward-chaining :trigger-terms ((fgl-object-kind x)))))