		Search-engine friendly clone of the ACL2 documentation.

Screens

Print-message-to-screen

Extend a screen with a message.

Signature
(print-message-to-screen message screen) → new-screen
Arguments: message — Guard (screen-messagep message).; screen — Guard (screenp screen).
Returns: new-screen — Type (screenp new-screen).

We append the message to the end of the list.

Definitions and Theorems

Function: print-message-to-screen

(defun print-message-to-screen (message screen)
  (declare (xargs :guard (and (screen-messagep message)
                              (screenp screen))))
  (let ((__function__ 'print-message-to-screen))
    (declare (ignorable __function__))
    (screen (append (screen->messages screen)
                    (list message)))))

Theorem: screenp-of-print-message-to-screen

(defthm screenp-of-print-message-to-screen
  (b* ((new-screen (print-message-to-screen message screen)))
    (screenp new-screen))
  :rule-classes :rewrite)

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

(defthm print-message-to-screen-of-screen-message-fix-message
  (equal (print-message-to-screen (screen-message-fix message)
                                  screen)
         (print-message-to-screen message screen)))

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

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

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

(defthm print-message-to-screen-of-screen-fix-screen
  (equal (print-message-to-screen message (screen-fix screen))
         (print-message-to-screen message screen)))

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

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