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