Tree for the null literal.
(null-literal-tree) → tree
This is used in grammar-null-literalp-when-null-literalp.
Function:
(defun null-literal-tree nil (declare (xargs :guard t)) (let ((__function__ 'null-literal-tree)) (declare (ignorable __function__)) (abnf::tree-nonleaf (abnf::rulename "null-literal") (list (list (abnf::tree-leafterm (string=>unicode *null-literal*)))))))
Theorem:
(defthm return-type-of-null-literal-tree (b* ((tree (null-literal-tree))) (abnf-tree-with-root-p tree "null-literal")) :rule-classes :rewrite)