		Search-engine friendly clone of the ACL2 documentation.

Elf64_sym

Elf64_sym-p

Recognizer for elf64_sym bit structures.

Signature
(elf64_sym-p x) → *

Definitions and Theorems

Function: elf64_sym-p

(defun elf64_sym-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'elf64_sym-p))
  (declare (ignorable __function__))
  (mbe
   :logic (unsigned-byte-p 192 x)
   :exec
   (and
    (natp x)
    (<
     x
     6277101735386680763835789423207666416102355444464034512896)))))

Theorem: elf64_sym-p-when-unsigned-byte-p

(defthm elf64_sym-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 192 x)
           (elf64_sym-p x)))

Theorem: unsigned-byte-p-when-elf64_sym-p

(defthm unsigned-byte-p-when-elf64_sym-p
  (implies (elf64_sym-p x)
           (unsigned-byte-p 192 x)))

Theorem: elf64_sym-p-compound-recognizer

(defthm elf64_sym-p-compound-recognizer
  (implies (elf64_sym-p x) (natp x))
  :rule-classes :compound-recognizer)