		Search-engine friendly clone of the ACL2 documentation.

Lexing-and-parsing

Output-file-lex-parse-p

Lexing and parsing of Leo output files.

This is analogous to file-lex-parse-p and input-file-lex-parse-p, but for output files instead of (code) files and input files.

Definitions and Theorems

Theorem: output-file-lex-parse-p-suff

(defthm output-file-lex-parse-p-suff
  (implies (and (abnf::tree-listp lexemes)
                (lexp ucodes lexemes)
                (output-file-parsep (filter-tokens lexemes)
                                    file))
           (output-file-lex-parse-p ucodes file)))

Theorem: booleanp-of-output-file-lex-parse-p

(defthm booleanp-of-output-file-lex-parse-p
  (b* ((yes/no (output-file-lex-parse-p ucodes file)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: output-file-lex-parse-p-of-unicode-list-fix-ucodes

(defthm output-file-lex-parse-p-of-unicode-list-fix-ucodes
  (equal (output-file-lex-parse-p (unicode-list-fix ucodes)
                                  file)
         (output-file-lex-parse-p ucodes file)))

Theorem: output-file-lex-parse-p-unicode-list-equiv-congruence-on-ucodes

(defthm
    output-file-lex-parse-p-unicode-list-equiv-congruence-on-ucodes
  (implies (unicode-list-equiv ucodes ucodes-equiv)
           (equal (output-file-lex-parse-p ucodes file)
                  (output-file-lex-parse-p ucodes-equiv file)))
  :rule-classes :congruence)

Theorem: output-file-lex-parse-p-of-tree-fix-file

(defthm output-file-lex-parse-p-of-tree-fix-file
  (equal (output-file-lex-parse-p ucodes (abnf::tree-fix file))
         (output-file-lex-parse-p ucodes file)))

Theorem: output-file-lex-parse-p-tree-equiv-congruence-on-file

(defthm output-file-lex-parse-p-tree-equiv-congruence-on-file
  (implies (abnf::tree-equiv file file-equiv)
           (equal (output-file-lex-parse-p ucodes file)
                  (output-file-lex-parse-p ucodes file-equiv)))
  :rule-classes :congruence)