		Search-engine friendly clone of the ACL2 documentation.

Valid-ext-info

Valid-ext-info->declared-in

Get the declared-in field from a valid-ext-info.

Signature
(valid-ext-info->declared-in x) → declared-in
Arguments: x — Guard (valid-ext-infop x).
Returns: declared-in — Type (filepath-setp declared-in).

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

Definitions and Theorems

Function: valid-ext-info->declared-in$inline

(defun valid-ext-info->declared-in$inline (x)
  (declare (xargs :guard (valid-ext-infop x)))
  (declare (xargs :guard t))
  (mbe :logic
       (b* ((x (and t x)))
         (filepath-set-fix (cdr (std::da-nth 1 x))))
       :exec (cdr (std::da-nth 1 x))))

Theorem: filepath-setp-of-valid-ext-info->declared-in

(defthm filepath-setp-of-valid-ext-info->declared-in
  (b* ((declared-in (valid-ext-info->declared-in$inline x)))
    (filepath-setp declared-in))
  :rule-classes :rewrite)

Theorem: valid-ext-info->declared-in$inline-of-valid-ext-info-fix-x

(defthm valid-ext-info->declared-in$inline-of-valid-ext-info-fix-x
  (equal (valid-ext-info->declared-in$inline (valid-ext-info-fix x))
         (valid-ext-info->declared-in$inline x)))

Theorem: valid-ext-info->declared-in$inline-valid-ext-info-equiv-congruence-on-x

(defthm
 valid-ext-info->declared-in$inline-valid-ext-info-equiv-congruence-on-x
 (implies (valid-ext-info-equiv x x-equiv)
          (equal (valid-ext-info->declared-in$inline x)
                 (valid-ext-info->declared-in$inline x-equiv)))
 :rule-classes :congruence)