		Search-engine friendly clone of the ACL2 documentation.

Dead-code-eliminator-execution

Funscope-result-dead

Eliminate dead code in errors and function scopes.

Signature
(funscope-result-dead funscope?) → new-funscope?
Arguments: funscope? — Guard (funscope-resultp funscope?).
Returns: new-funscope? — Type (funscope-resultp new-funscope?).

We transform function scopes and leave errors unchanged.

Definitions and Theorems

Function: funscope-result-dead

(defun funscope-result-dead (funscope?)
  (declare (xargs :guard (funscope-resultp funscope?)))
  (let ((__function__ 'funscope-result-dead))
    (declare (ignorable __function__))
    (b* ((funscope? (funscope-result-fix funscope?)))
      (if (reserrp funscope?)
          funscope?
        (funscope-dead funscope?)))))

Theorem: funscope-resultp-of-funscope-result-dead

(defthm funscope-resultp-of-funscope-result-dead
  (b* ((new-funscope? (funscope-result-dead funscope?)))
    (funscope-resultp new-funscope?))
  :rule-classes :rewrite)

Theorem: funscope-result-dead-of-funscope-result-fix-funscope?

(defthm funscope-result-dead-of-funscope-result-fix-funscope?
  (equal (funscope-result-dead (funscope-result-fix funscope?))
         (funscope-result-dead funscope?)))

Theorem: funscope-result-dead-funscope-result-equiv-congruence-on-funscope?

(defthm
 funscope-result-dead-funscope-result-equiv-congruence-on-funscope?
 (implies (funscope-result-equiv funscope? funscope?-equiv)
          (equal (funscope-result-dead funscope?)
                 (funscope-result-dead funscope?-equiv)))
 :rule-classes :congruence)