		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-charval-info

Generate the information for a character value notation.

Signature
(deftreeops-gen-charval-info charval prefix) → info
Arguments: charval — Guard (char-val-p charval).; prefix — Guard (common-lisp::symbolp prefix).
Returns: info — Type (deftreeops-charval-infop info).

Definitions and Theorems

Function: deftreeops-gen-charval-info

(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: deftreeops-charval-infop-of-deftreeops-gen-charval-info

(defthm deftreeops-charval-infop-of-deftreeops-gen-charval-info
  (b* ((info (deftreeops-gen-charval-info charval prefix)))
    (deftreeops-charval-infop info))
  :rule-classes :rewrite)