|
|
|---|
|
|
|
|---|
The parsed old 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 Unicode character set.
Function:
(defun untranslate-preprocess-*grammar-old* (acl2::term acl2::wrld) (if (equal acl2::term (list 'quote *grammar-old*)) '*grammar-old* (abnf::untranslate-preprocess-*grammar* acl2::term acl2::wrld)))
Theorem:
(defthm rulelist-wfp-of-*grammar-old* (abnf::rulelist-wfp *grammar-old*))
Theorem:
(defthm rulelist-closedp-of-*grammar-old* (abnf::rulelist-closedp *grammar-old*))
Theorem:
(defthm unicode-only-*grammar-old* (abnf::rulelist-in-termset-p *grammar-old* (integers-from-to 0 1114111)))