Generate the alist from character value notation to character value notation information from a list of rules.
(deftreeops-gen-charval-info-alist rules prefix) → infos
We obtain the set of character value notations from the rules, and then we generate an alist from the set.
Function:
(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:
(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:
(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:
(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)