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