Generate a shallowly embedded ACL2 quoted number.
(atj-gen-shallow-number number) → expr
This is just a reference to the field for the quoted number.
Function:
(defun atj-gen-shallow-number (number) (declare (xargs :guard (acl2-numberp number))) (let ((__function__ 'atj-gen-shallow-number)) (declare (ignorable __function__)) (jexpr-name (atj-gen-shallow-number-field-name number))))
Theorem:
(defthm jexprp-of-atj-gen-shallow-number (b* ((expr (atj-gen-shallow-number number))) (jexprp expr)) :rule-classes :rewrite)