		Search-engine friendly clone of the ACL2 documentation.

Init-screen

Initial screen.

This is empty.

Function: init-screen

(defun init-screen nil
  (declare (xargs :guard t))
  (let ((__function__ 'init-screen))
    (declare (ignorable __function__))
    (screen nil)))

Theorem: screenp-of-init-screen

(defthm screenp-of-init-screen
  (b* ((screen (init-screen)))
    (screenp screen))
  :rule-classes :rewrite)