The PDF grammar rules from our grammar.
The file
The PDF grammar rules are well-formed and closed.
We keep this constant unexpanded in output.
Function:
(defun untranslate-preprocess-*pdf-grammar-rules* (acl2::term acl2::wrld) (if (equal acl2::term (list 'quote *pdf-grammar-rules*)) '*pdf-grammar-rules* (untranslate-preprocess-*grammar* acl2::term acl2::wrld)))
Theorem:
(defthm rulelist-wfp-of-*pdf-grammar-rules* (rulelist-wfp *pdf-grammar-rules*))
Theorem:
(defthm rulelist-closedp-of-*pdf-grammar-rules* (rulelist-closedp *pdf-grammar-rules*))