		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-annop

Attrib-name-annop

Signature
(attrib-name-annop attrib-name) → fty::result
Arguments: attrib-name — Guard (attrib-namep attrib-name).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: attrib-name-annop

(defun attrib-name-annop (attrib-name)
  (declare (xargs :guard (attrib-namep attrib-name)))
  (declare (ignorable attrib-name))
  (let ((__function__ 'attrib-name-annop))
    (declare (ignorable __function__))
    (attrib-name-case
         attrib-name
         :ident (ident-annop (attrib-name-ident->ident attrib-name))
         :keyword t)))

Theorem: booleanp-of-attrib-name-annop

(defthm booleanp-of-attrib-name-annop
  (b* ((fty::result (attrib-name-annop attrib-name)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: attrib-name-annop-of-attrib-name-fix-attrib-name

(defthm attrib-name-annop-of-attrib-name-fix-attrib-name
  (equal (attrib-name-annop (attrib-name-fix attrib-name))
         (attrib-name-annop attrib-name)))

Theorem: attrib-name-annop-attrib-name-equiv-congruence-on-attrib-name

(defthm
      attrib-name-annop-attrib-name-equiv-congruence-on-attrib-name
  (implies (attrib-name-equiv attrib-name attrib-name-equiv)
           (equal (attrib-name-annop attrib-name)
                  (attrib-name-annop attrib-name-equiv)))
  :rule-classes :congruence)