Generate a shallowly embedded ACL2 value.
(atj-gen-shallow-value value qpairs pkg-class-names curr-pkg guards$) → expr
Function:
(defun atj-gen-shallow-value (value qpairs pkg-class-names curr-pkg guards$) (declare (xargs :guard (and (cons-pos-alistp qpairs) (string-string-alistp pkg-class-names) (stringp curr-pkg) (booleanp guards$)))) (let ((__function__ 'atj-gen-shallow-value)) (declare (ignorable __function__)) (cond ((acl2-numberp value) (atj-gen-shallow-number value)) ((characterp value) (atj-gen-shallow-char value guards$)) ((stringp value) (atj-gen-shallow-string value guards$)) ((symbolp value) (atj-gen-shallow-symbol value pkg-class-names curr-pkg guards$)) ((consp value) (atj-gen-shallow-cons value qpairs)) (t (prog2$ (raise "Internal error: ~x0 is not a recognized value." value) (jexpr-name ""))))))
Theorem:
(defthm jexprp-of-atj-gen-shallow-value (b* ((expr (atj-gen-shallow-value value qpairs pkg-class-names curr-pkg guards$))) (jexprp expr)) :rule-classes :rewrite)