Check if a
(unicode-input-character-tree-is-escape-p tree) → yes/no
That is, check if the (only) subtree of the tree
is a
Function:
(defun unicode-input-character-tree-is-escape-p (tree) (declare (xargs :guard (abnf-tree-with-root-p tree "unicode-input-character"))) (abnf-tree-with-root-p (caar (abnf::tree-nonleaf->branches tree)) "unicode-escape"))
Theorem:
(defthm booleanp-of-unicode-input-character-tree-is-escape-p (b* ((yes/no (unicode-input-character-tree-is-escape-p tree))) (booleanp yes/no)) :rule-classes :rewrite)