		Search-engine friendly clone of the ACL2 documentation.

Expr

Expr-kind

Get the kind (tag) of a expr structure.

Signature
(expr-kind x) → kind
Arguments: x — Guard (exprp x).

Definitions and Theorems

Function: expr-kind$inline

(defun expr-kind$inline (x)
  (declare (xargs :guard (exprp x)))
  (let ((__function__ 'expr-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :ident))
                       :ident)
                      ((eq (car x) :const) :const)
                      ((eq (car x) :arrsub) :arrsub)
                      ((eq (car x) :call) :call)
                      ((eq (car x) :member) :member)
                      ((eq (car x) :memberp) :memberp)
                      ((eq (car x) :postinc) :postinc)
                      ((eq (car x) :postdec) :postdec)
                      ((eq (car x) :preinc) :preinc)
                      ((eq (car x) :predec) :predec)
                      ((eq (car x) :unary) :unary)
                      ((eq (car x) :cast) :cast)
                      ((eq (car x) :binary) :binary)
                      (t :cond))
         :exec (car x))))

Theorem: expr-kind-possibilities

(defthm expr-kind-possibilities
 (or (equal (expr-kind x) :ident)
     (equal (expr-kind x) :const)
     (equal (expr-kind x) :arrsub)
     (equal (expr-kind x) :call)
     (equal (expr-kind x) :member)
     (equal (expr-kind x) :memberp)
     (equal (expr-kind x) :postinc)
     (equal (expr-kind x) :postdec)
     (equal (expr-kind x) :preinc)
     (equal (expr-kind x) :predec)
     (equal (expr-kind x) :unary)
     (equal (expr-kind x) :cast)
     (equal (expr-kind x) :binary)
     (equal (expr-kind x) :cond))
 :rule-classes ((:forward-chaining :trigger-terms ((expr-kind x)))))