		Search-engine friendly clone of the ACL2 documentation.

Null-literal-grammar-validation

Null-literal-tree

Tree for the null literal.

Signature
(null-literal-tree) → tree
Returns: tree — Type (abnf-tree-with-root-p tree "null-literal").

This is used in grammar-null-literalp-when-null-literalp.

Definitions and Theorems

Function: null-literal-tree

(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: return-type-of-null-literal-tree

(defthm return-type-of-null-literal-tree
  (b* ((tree (null-literal-tree)))
    (abnf-tree-with-root-p tree "null-literal"))
  :rule-classes :rewrite)