		Search-engine friendly clone of the ACL2 documentation.

Load-funct

Load-funct-kind

Get the kind (tag) of a load-funct structure.

Signature
(load-funct-kind x) → kind
Arguments: x — Guard (load-funct-p x).

Definitions and Theorems

Function: load-funct-kind$inline

(defun load-funct-kind$inline (x)
  (declare (xargs :guard (load-funct-p x)))
  (let ((__function__ 'load-funct-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :lb)) :lb)
                      ((eq (car x) :lbu) :lbu)
                      ((eq (car x) :lh) :lh)
                      ((eq (car x) :lhu) :lhu)
                      ((eq (car x) :lw) :lw)
                      ((eq (car x) :lwu) :lwu)
                      (t :ld))
         :exec (car x))))

Theorem: load-funct-kind-possibilities

(defthm load-funct-kind-possibilities
  (or (equal (load-funct-kind x) :lb)
      (equal (load-funct-kind x) :lbu)
      (equal (load-funct-kind x) :lh)
      (equal (load-funct-kind x) :lhu)
      (equal (load-funct-kind x) :lw)
      (equal (load-funct-kind x) :lwu)
      (equal (load-funct-kind x) :ld))
  :rule-classes
  ((:forward-chaining :trigger-terms ((load-funct-kind x)))))