		Search-engine friendly clone of the ACL2 documentation.

Parser-interface

Statement-parses-same-fringe?

Checks if the given string can be parsed to a Leo statement CST.

Signature
(statement-parses-same-fringe? statement-string) → yes/no
Arguments: statement-string — Guard (stringp statement-string).
Returns: yes/no — Type (booleanp yes/no).

Same as statement-parses?, but this does some additional checks, so it is better for testing.

Definitions and Theorems

Function: statement-parses-same-fringe?

(defun statement-parses-same-fringe? (statement-string)
 (declare (xargs :guard (stringp statement-string)))
 (let ((__function__ 'statement-parses-same-fringe?))
  (declare (ignorable __function__))
  (b* (((mv tree? lexemes)
        (parse-fragment-to-cst+ "statement" statement-string)))
   (and
     (abnf::treep tree?)
     (abnf-tree-with-root-p tree? "statement")
     (abnf-tree-list-with-root-p lexemes "lexeme")
     (equal
          (abnf::tree-list->string lexemes)
          (acl2::utf8=>ustring (string=>nats statement-string)))))))

Theorem: booleanp-of-statement-parses-same-fringe?

(defthm booleanp-of-statement-parses-same-fringe?
  (b* ((yes/no (statement-parses-same-fringe? statement-string)))
    (booleanp yes/no))
  :rule-classes :rewrite)