Generate the information for a character value notation.
(deftreeops-gen-charval-info charval prefix) → info
Function:
(defun deftreeops-gen-charval-info (charval prefix) (declare (xargs :guard (and (char-val-p charval) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-charval-info)) (declare (ignorable __function__)) (b* ((leafterm-thm (packn-pos (list prefix '- (pretty-print-char-val charval) '-leafterm) prefix))) (make-deftreeops-charval-info :leafterm-thm leafterm-thm))))
Theorem:
(defthm deftreeops-charval-infop-of-deftreeops-gen-charval-info (b* ((info (deftreeops-gen-charval-info charval prefix))) (deftreeops-charval-infop info)) :rule-classes :rewrite)