		Search-engine friendly clone of the ACL2 documentation.

Fsuffix

Fsuffixp

Recognizer for fsuffix structures.

Signature
(fsuffixp f) → *

Definitions and Theorems

Function: fsuffixp

(defun fsuffixp (f)
  (declare (xargs :guard t))
  (and (consp f)
       (cond ((or (atom f) (eq (car f) :locase-f))
              (and (eq (cdr f) nil) (b* nil t)))
             ((eq (car f) :upcase-f)
              (and (eq (cdr f) nil) (b* nil t)))
             ((eq (car f) :locase-l)
              (and (eq (cdr f) nil) (b* nil t)))
             ((eq (car f) :upcase-l)
              (and (eq (cdr f) nil) (b* nil t)))
             ((eq (car f) :locase-f16)
              (and (b* ((x (cdr f))) (booleanp x))))
             ((eq (car f) :locase-f32)
              (and (b* ((x (cdr f))) (booleanp x))))
             ((eq (car f) :locase-f64)
              (and (b* ((x (cdr f))) (booleanp x))))
             ((eq (car f) :locase-f128)
              (and (b* ((x (cdr f))) (booleanp x))))
             ((eq (car f) :upcase-f16)
              (and (b* ((x (cdr f))) (booleanp x))))
             ((eq (car f) :upcase-f32)
              (and (b* ((x (cdr f))) (booleanp x))))
             ((eq (car f) :upcase-f64)
              (and (b* ((x (cdr f))) (booleanp x))))
             (t (and (eq (car f) :upcase-f128)
                     (and)
                     (b* ((x (cdr f))) (booleanp x)))))))

Theorem: consp-when-fsuffixp

(defthm consp-when-fsuffixp
  (implies (fsuffixp f) (consp f))
  :rule-classes :compound-recognizer)