Generate Java code to build a deeply embedded ACL2 variable.
Function:
(defun atj-gen-deep-var (var) (declare (xargs :guard (symbolp var))) (let ((__function__ 'atj-gen-deep-var)) (declare (ignorable __function__)) (jexpr-smethod *aij-type-var* "make" (list (atj-gen-symbol var t nil)))))
Theorem:
(defthm jexprp-of-atj-gen-deep-var (b* ((expr (atj-gen-deep-var var))) (jexprp expr)) :rule-classes :rewrite)