All the JSON grammar rules, including the referenced ABNF core rules.
These are obtained by plugging the core rules into the IMAP rules.
These rules are well-formed and closed.
These rules generate terminal strings consisting only of Unicode codes,
i.e. natural numbers between 0 and
We use ACL2::add-const-to-untranslate-preprocess to keep this constant unexpanded in output.
Definition:
(defconst *all-grammar-rules* (abnf::plug-rules *grammar-rules* abnf::*core-rules*))
Function:
(defun untranslate-preprocess-*all-grammar-rules* (acl2::term acl2::wrld) (if (equal acl2::term (list 'quote *all-grammar-rules*)) '*all-grammar-rules* (untranslate-preprocess-*grammar-rules* acl2::term acl2::wrld)))
Theorem:
(defthm rulelist-wfp-of-*all-grammar-rules* (abnf::rulelist-wfp *all-grammar-rules*))
Theorem:
(defthm rulelist-closedp-of-*all-grammar-rules* (abnf::rulelist-closedp *all-grammar-rules*))
Theorem:
(defthm unicode-only-*all-grammar-rules* (abnf::rulelist-in-termset-p *all-grammar-rules* (acl2::integers-from-to 0 1114111)))