|
|
|---|
|
|
|
|---|
The parsed new ABNF grammar of Yul.
We parse the grammar file to obtain an ABNF grammar value.
We prove that the grammar is well-formed, is closed, and only generates terminals in the ASCII character set.
Function:
(defun untranslate-preprocess-*grammar-new* (acl2::term acl2::wrld) (if (equal acl2::term (list 'quote *grammar-new*)) '*grammar-new* (abnf::untranslate-preprocess-*grammar* acl2::term acl2::wrld)))
Theorem:
(defthm rulelist-wfp-of-*grammar-new* (abnf::rulelist-wfp *grammar-new*))
Theorem:
(defthm rulelist-closedp-of-*grammar-new* (abnf::rulelist-closedp *grammar-new*))
Theorem:
(defthm ascii-only-*grammar-new* (abnf::rulelist-in-termset-p *grammar-new* (acl2::integers-from-to 0 127)))