		Search-engine friendly clone of the ACL2 documentation.

Spec/qual-attrib

Spec/qual-attrib->spec

Get the spec field from a spec/qual-attrib.

Signature
(spec/qual-attrib->spec x) → spec
Arguments: x — Guard (spec/qual-p x).
Returns: spec — Type (attrib-specp spec).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: spec/qual-attrib->spec$inline

(defun spec/qual-attrib->spec$inline (x)
  (declare (xargs :guard (spec/qual-p x)))
  (declare (xargs :guard (equal (spec/qual-kind x) :attrib)))
  (mbe :logic
       (b* ((x (and (equal (spec/qual-kind x) :attrib)
                    x)))
         (attrib-spec-fix (cdr x)))
       :exec (cdr x)))

Theorem: attrib-specp-of-spec/qual-attrib->spec

(defthm attrib-specp-of-spec/qual-attrib->spec
  (b* ((spec (spec/qual-attrib->spec$inline x)))
    (attrib-specp spec))
  :rule-classes :rewrite)

Theorem: spec/qual-attrib->spec$inline-of-spec/qual-fix-x

(defthm spec/qual-attrib->spec$inline-of-spec/qual-fix-x
  (equal (spec/qual-attrib->spec$inline (spec/qual-fix x))
         (spec/qual-attrib->spec$inline x)))

Theorem: spec/qual-attrib->spec$inline-spec/qual-equiv-congruence-on-x

(defthm
      spec/qual-attrib->spec$inline-spec/qual-equiv-congruence-on-x
  (implies (spec/qual-equiv x x-equiv)
           (equal (spec/qual-attrib->spec$inline x)
                  (spec/qual-attrib->spec$inline x-equiv)))
  :rule-classes :congruence)

Theorem: spec/qual-attrib->spec-when-wrong-kind

(defthm spec/qual-attrib->spec-when-wrong-kind
  (implies (not (equal (spec/qual-kind x) :attrib))
           (equal (spec/qual-attrib->spec x)
                  (attrib-spec-fix nil))))