Abstract a
(abs-unicode-input-character tree) → unicode
Whether the tree is a raw character or a Unicode escape, it always denotes a single Unicode character, which we abstract this kind of trees to.
A
Function:
(defun abs-unicode-input-character (tree) (declare (xargs :guard (abnf-tree-with-root-p tree "unicode-input-character"))) (let ((__function__ 'abs-unicode-input-character)) (declare (ignorable __function__)) (b* ((subtree (caar (abnf::tree-nonleaf->branches tree)))) (if (abnf-tree-with-root-p subtree "unicode-escape") (abs-unicode-escape subtree) (abs-raw-input-character subtree)))))
Theorem:
(defthm unicodep-of-abs-unicode-input-character (implies (and (abnf-tree-with-root-p tree '"unicode-input-character")) (b* ((unicode (abs-unicode-input-character tree))) (unicodep unicode))) :rule-classes :rewrite)