Initial tag environment.
(tag-env-init) → env
This is empty.
Function:
(defun tag-env-init nil (declare (xargs :guard t)) (let ((__function__ 'tag-env-init)) (declare (ignorable __function__)) nil))
Theorem:
(defthm tag-envp-of-tag-env-init (b* ((env (tag-env-init))) (tag-envp env)) :rule-classes :rewrite)