		Search-engine friendly clone of the ACL2 documentation.

Init-struct-denv

Initial dynamic struct environment.

This is empty.

Function: init-struct-denv

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

Theorem: struct-denvp-of-init-struct-denv

(defthm struct-denvp-of-init-struct-denv
  (b* ((env (init-struct-denv)))
    (struct-denvp env))
  :rule-classes :rewrite)