		Search-engine friendly clone of the ACL2 documentation.

Execution

Exec-print

Execute the printing of a message on the screen.

Signature
(exec-print message env) → new-env
Arguments: message — Guard (screen-messagep message).; env — Guard (denvp env).
Returns: new-env — Type (denvp new-env).

Definitions and Theorems

Function: exec-print

(defun exec-print (message env)
  (declare (xargs :guard (and (screen-messagep message)
                              (denvp env))))
  (let ((__function__ 'exec-print))
    (declare (ignorable __function__))
    (b* ((screen (denv->screen env))
         (new-screen (print-message-to-screen message screen))
         (new-env (change-denv env :screen new-screen)))
      new-env)))

Theorem: denvp-of-exec-print

(defthm denvp-of-exec-print
  (b* ((new-env (exec-print message env)))
    (denvp new-env))
  :rule-classes :rewrite)

Theorem: exec-print-of-screen-message-fix-message

(defthm exec-print-of-screen-message-fix-message
  (equal (exec-print (screen-message-fix message)
                     env)
         (exec-print message env)))

Theorem: exec-print-screen-message-equiv-congruence-on-message

(defthm exec-print-screen-message-equiv-congruence-on-message
  (implies (screen-message-equiv message message-equiv)
           (equal (exec-print message env)
                  (exec-print message-equiv env)))
  :rule-classes :congruence)

Theorem: exec-print-of-denv-fix-env

(defthm exec-print-of-denv-fix-env
  (equal (exec-print message (denv-fix env))
         (exec-print message env)))

Theorem: exec-print-denv-equiv-congruence-on-env

(defthm exec-print-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-print message env)
                  (exec-print message env-equiv)))
  :rule-classes :congruence)