		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-execution-rules

Atc-exec-expr-when-pure-rules

Rules for executing pure expressions with exec-expr.

Definitions and Theorems

Theorem: exec-expr-when-pure

(defthm exec-expr-when-pure
  (implies (and (syntaxp (quotep e))
                (expr-purep e)
                (integerp limit)
                (>= limit (expr-pure-limit e))
                (compustatep compst)
                (equal eval (exec-expr-pure e compst))
                (expr-valuep eval))
           (equal (exec-expr e compst fenv limit)
                  (mv eval compst))))