Parse tree of the text that contains the concrete syntax rules of ABNF.
The file
We use add-const-to-untranslate-preprocess to keep this constant unexpanded in output.
Function:
(defun untranslate-preprocess-*concrete-syntax-rules-parsed* (acl2::term acl2::wrld) (if (equal acl2::term (list 'quote *concrete-syntax-rules-parsed*)) '*concrete-syntax-rules-parsed* (untranslate-preprocess-*core-rules-parsed* acl2::term acl2::wrld)))
Theorem:
(defthm treep-of-*concrete-syntax-rules-parsed* (treep *concrete-syntax-rules-parsed*))