		Search-engine friendly clone of the ACL2 documentation.

Pdf-example

pdf-grammar-rules

The PDF grammar rules from our grammar.

The file pdf.abnf contains the grammar rules. The ABNF grammar parser and abstractor are used to build an ACL2 representation of the PDF grammar rules.

The PDF grammar rules are well-formed and closed.

We keep this constant unexpanded in output.

Definitions and Theorems

Function: untranslate-preprocess-*pdf-grammar-rules*

(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: rulelist-wfp-of-*pdf-grammar-rules*

(defthm rulelist-wfp-of-*pdf-grammar-rules*
  (rulelist-wfp *pdf-grammar-rules*))

Theorem: rulelist-closedp-of-*pdf-grammar-rules*

(defthm rulelist-closedp-of-*pdf-grammar-rules*
  (rulelist-closedp *pdf-grammar-rules*))

Subtopics

*pdf-grammar-rules*-tree-operations: Tree operations specialized to *pdf-grammar-rules*.