		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-charval-info-alist

Generate the alist from character value notation to character value notation information from a list of rules.

Signature
(deftreeops-gen-charval-info-alist rules prefix) → infos
Arguments: rules — Guard (rulelistp rules).; prefix — Guard (common-lisp::symbolp prefix).
Returns: infos — Type (deftreeops-charval-info-alistp infos).

We obtain the set of character value notations from the rules, and then we generate an alist from the set.

Definitions and Theorems

Function: deftreeops-gen-charval-info-alist-aux

(defun deftreeops-gen-charval-info-alist-aux (charvals prefix)
 (declare (xargs :guard (and (char-val-setp charvals)
                             (common-lisp::symbolp prefix))))
 (let ((__function__ 'deftreeops-gen-charval-info-alist-aux))
  (declare (ignorable __function__))
  (b* (((when (emptyp charvals)) nil)
       (charval (head charvals))
       (info (deftreeops-gen-charval-info charval prefix))
       (infos (deftreeops-gen-charval-info-alist-aux (tail charvals)
                                                     prefix)))
    (acons charval info infos))))

Theorem: deftreeops-charval-info-alistp-of-deftreeops-gen-charval-info-alist-aux

(defthm
 deftreeops-charval-info-alistp-of-deftreeops-gen-charval-info-alist-aux
 (implies
   (char-val-setp charvals)
   (b*
    ((info (deftreeops-gen-charval-info-alist-aux charvals prefix)))
    (deftreeops-charval-info-alistp info)))
 :rule-classes :rewrite)

Function: deftreeops-gen-charval-info-alist

(defun deftreeops-gen-charval-info-alist (rules prefix)
 (declare (xargs :guard (and (rulelistp rules)
                             (common-lisp::symbolp prefix))))
 (let ((__function__ 'deftreeops-gen-charval-info-alist))
   (declare (ignorable __function__))
   (deftreeops-gen-charval-info-alist-aux (rulelist-char-vals rules)
                                          prefix)))

Theorem: deftreeops-charval-info-alistp-of-deftreeops-gen-charval-info-alist

(defthm
 deftreeops-charval-info-alistp-of-deftreeops-gen-charval-info-alist
 (b* ((infos (deftreeops-gen-charval-info-alist rules prefix)))
   (deftreeops-charval-info-alistp infos))
 :rule-classes :rewrite)