• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
        • Atj
        • Aij
        • Language
          • Syntax
            • Grammar
              • Cst-statement-without-trailing-substatement-conc?
              • Abnf-tree-with-root-p
              • *grammar*
              • Cst-statement-expression-conc?
              • Cst-statement-no-short-if-conc?
              • Cst-statement-conc?
              • Cst-literal-conc?
              • Cst-class-body-declaration-conc?
              • Cst-postfix-expression-conc?
              • Cst-import-declaration-conc?
              • Cst-integer-literal-conc?
              • Cst-token-conc?
              • Cst-unann-reference-type-conc?
              • Cst-block-statement-conc?
              • Cst-unann-class-or-interface-type-conc?
              • Cst-reference-type-conc?
              • Cst-left-hand-side-conc?
              • Cst-input-element-conc?
              • Cst-element-value-conc?
              • Cst-for-statement-no-short-if-conc?
              • Cst-floating-point-literal-conc?
              • Cst-annotation-conc?
              • Cst-variable-initializer-conc?
              • Cst-unicode-input-character-conc?
              • Cst-interface-declaration-conc?
              • Cst-class-or-interface-type-conc?
              • Cst-assignment-expression-conc?
              • Cst-string-character-conc?
              • Cst-statement-without-trailing-substatement-conc13-rep-elem
              • Cst-statement-without-trailing-substatement-conc12-rep-elem
              • Cst-statement-without-trailing-substatement-conc11-rep-elem
              • Cst-statement-without-trailing-substatement-conc10-rep-elem
              • Cst-not-star-not-slash-conc?
              • Cst-list-list-conc-matchp$
              • Cst-compilation-unit-conc?
              • Cst-class-declaration-conc?
              • Cst-variable-access-conc?
              • Cst-unqualified-class-instance-creation-expression-conc
              • Cst-statement-without-trailing-substatement-conc9-rep-elem
              • Cst-statement-without-trailing-substatement-conc9-rep
              • Cst-statement-without-trailing-substatement-conc8-rep-elem
              • Cst-statement-without-trailing-substatement-conc8-rep
              • Cst-statement-without-trailing-substatement-conc7-rep-elem
              • Cst-statement-without-trailing-substatement-conc7-rep
              • Cst-statement-without-trailing-substatement-conc6-rep-elem
              • Cst-statement-without-trailing-substatement-conc6-rep
              • Cst-statement-without-trailing-substatement-conc5-rep-elem
              • Cst-statement-without-trailing-substatement-conc5-rep
              • Cst-statement-without-trailing-substatement-conc4-rep-elem
              • Cst-statement-without-trailing-substatement-conc4-rep
              • Cst-statement-without-trailing-substatement-conc3-rep-elem
              • Cst-statement-without-trailing-substatement-conc3-rep
              • Cst-statement-without-trailing-substatement-conc2-rep-elem
              • Cst-statement-without-trailing-substatement-conc2-rep
              • Cst-statement-without-trailing-substatement-conc13-rep
              • Cst-statement-without-trailing-substatement-conc12-rep
              • Cst-statement-without-trailing-substatement-conc11-rep
              • Cst-statement-without-trailing-substatement-conc10-rep
              • Cst-statement-without-trailing-substatement-conc1-rep-elem
              • Cst-statement-without-trailing-substatement-conc1-rep
              • Cst-list-list-alt-matchp$
              • Cst-for-statement-conc?
              • Cst-exception-type-conc?
              • Cst-unann-type-conc?
              • Cst-type-argument-conc?
              • Cst-statement-without-trailing-substatement-conc13
              • Cst-statement-without-trailing-substatement-conc12
              • Cst-statement-without-trailing-substatement-conc11
              • Cst-statement-without-trailing-substatement-conc10
              • Cst-numeric-type-conc?
              • Cst-lambda-body-conc?
              • Cst-expression-conc?
              • Cst-unann-class-or-interface-type-conc2-rep-elem
              • Cst-unann-class-or-interface-type-conc1-rep-elem
              • Cst-statement-without-trailing-substatement-conc9
              • Cst-statement-without-trailing-substatement-conc8
              • Cst-statement-without-trailing-substatement-conc7
              • Cst-statement-without-trailing-substatement-conc6
              • Cst-statement-without-trailing-substatement-conc5
              • Cst-statement-without-trailing-substatement-conc4
              • Cst-statement-without-trailing-substatement-conc3
              • Cst-statement-without-trailing-substatement-conc2
              • Cst-statement-without-trailing-substatement-conc1
              • Cst-primary-conc?
              • Cst-not-star-conc?
              • Cst-list-rep-matchp$
              • Cst-list-elem-matchp$
              • Cst-for-init-conc?
              • Cst-comment-conc?
              • Cst-unann-class-or-interface-type-conc2-rep
              • Cst-unann-class-or-interface-type-conc1-rep
              • Cst-type-conc?
              • Cst-local-variable-declaration-statement-conc
              • Cst-for-statement-no-short-if-conc2-rep-elem
              • Cst-for-statement-no-short-if-conc1-rep-elem
              • Cst-class-or-interface-type-to-instantiate-conc
              • Cst-annotation-type-element-declaration-conc
              • Cst-variable-initializer-conc2-rep-elem
              • Cst-variable-initializer-conc1-rep-elem
              • Cst-unqualified-method-identifier-conc-rep-elem
              • Cst-unqualified-method-identifier-conc-rep
              • Cst-unicode-input-character-conc2-rep-elem
              • Cst-unicode-input-character-conc2-rep
              • Cst-unicode-input-character-conc1-rep-elem
              • Cst-unicode-input-character-conc1-rep
              • Cst-unann-reference-type-conc3-rep-elem
              • Cst-unann-reference-type-conc2-rep-elem
              • Cst-unann-reference-type-conc1-rep-elem
              • Cst-unann-class-or-interface-type-conc2
              • Cst-unann-class-or-interface-type-conc1
              • Cst-type-import-on-demand-declaration-conc
              • Cst-static-import-on-demand-declaration-conc
              • Cst-statement-no-short-if-conc5-rep-elem
              • Cst-statement-no-short-if-conc4-rep-elem
              • Cst-statement-no-short-if-conc3-rep-elem
              • Cst-statement-no-short-if-conc2-rep-elem
              • Cst-statement-no-short-if-conc1-rep-elem
              • Cst-statement-expression-conc7-rep-elem
              • Cst-statement-expression-conc6-rep-elem
              • Cst-statement-expression-conc5-rep-elem
              • Cst-statement-expression-conc4-rep-elem
              • Cst-statement-expression-conc3-rep-elem
              • Cst-statement-expression-conc2-rep-elem
              • Cst-statement-expression-conc1-rep-elem
              • Cst-single-type-import-declaration-conc
              • Cst-single-static-import-declaration-conc
              • Cst-interface-declaration-conc2-rep-elem
              • Cst-interface-declaration-conc1-rep-elem
              • Cst-if-then-else-statement-no-short-if-conc
              • Cst-hexadecimal-floating-point-literal-conc
              • Cst-for-statement-no-short-if-conc2-rep
              • Cst-for-statement-no-short-if-conc2
              • Cst-for-statement-no-short-if-conc1-rep
              • Cst-for-statement-no-short-if-conc1
              • Cst-floating-point-literal-conc2-rep-elem
              • Cst-floating-point-literal-conc2-rep
              • Cst-floating-point-literal-conc1-rep-elem
              • Cst-floating-point-literal-conc1-rep
              • Cst-enhanced-for-statement-no-short-if-conc
              • Cst-element-value-array-initializer-conc
              • Cst-class-or-interface-type-conc2-rep-elem
              • Cst-class-or-interface-type-conc2-rep
              • Cst-class-or-interface-type-conc1-rep-elem
              • Cst-class-or-interface-type-conc1-rep
              • Cst-class-body-declaration-conc4-rep-elem
              • Cst-class-body-declaration-conc3-rep-elem
              • Cst-class-body-declaration-conc2-rep-elem
              • Cst-class-body-declaration-conc1-rep-elem
              • Cst-basic-for-statement-no-short-if-conc
              • Cst-assignment-expression-conc2-rep-elem
              • Cst-assignment-expression-conc1-rep-elem
              • Cst-while-statement-no-short-if-conc
              • Cst-variable-initializer-conc2-rep
              • Cst-variable-initializer-conc1-rep
              • Cst-unqualified-method-identifier-conc
              • Cst-unicode-input-character-conc2
              • Cst-unicode-input-character-conc1
              • Cst-unann-reference-type-conc3-rep
              • Cst-unann-reference-type-conc2-rep
              • Cst-unann-reference-type-conc1-rep
              • Cst-unann-reference-type-conc1
              • Cst-type-parameter-modifier-conc-rep-elem
              • Cst-try-with-resources-statement-conc
              • Cst-switch-block-statement-group-conc
              • Cst-string-character-conc2-rep-elem
              • Cst-string-character-conc1-rep-elem
              • Cst-statement-no-short-if-conc5-rep
              • Cst-statement-no-short-if-conc5
              • Cst-statement-no-short-if-conc4-rep
              • Cst-statement-no-short-if-conc4
              • Cst-statement-no-short-if-conc3-rep
              • Cst-statement-no-short-if-conc3
              • Cst-statement-no-short-if-conc2-rep
              • Cst-statement-no-short-if-conc2
              • Cst-statement-no-short-if-conc1-rep
              • Cst-statement-no-short-if-conc1
              • Cst-statement-expression-conc7-rep
              • Cst-statement-expression-conc7
              • Cst-statement-expression-conc6-rep
              • Cst-statement-expression-conc5-rep
              • Cst-statement-expression-conc5
              • Cst-statement-expression-conc4-rep
              • Cst-statement-expression-conc4
              • Cst-statement-expression-conc3-rep
              • Cst-statement-expression-conc3
              • Cst-statement-expression-conc2-rep
              • Cst-statement-expression-conc2
              • Cst-statement-expression-conc1-rep
              • Cst-postfix-expression-conc4-rep-elem
              • Cst-postfix-expression-conc4-rep
              • Cst-postfix-expression-conc3-rep-elem
              • Cst-postfix-expression-conc3-rep
              • Cst-postfix-expression-conc2-rep-elem
              • Cst-postfix-expression-conc2-rep
              • Cst-postfix-expression-conc1-rep-elem
              • Cst-postfix-expression-conc1-rep
              • Cst-octal-digits-and-underscores-conc
              • Cst-not-star-not-slash-conc2-rep-elem
              • Cst-not-star-not-slash-conc2-rep
              • Cst-not-star-not-slash-conc1-rep-elem
              • Cst-not-star-not-slash-conc1-rep
              • Cst-normal-interface-declaration-conc
              • Cst-matchp$
              • Cst-local-variable-declaration-conc
              • Cst-labeled-statement-no-short-if-conc
              • Cst-interface-method-declaration-conc
              • Cst-interface-declaration-conc2-rep
              • Cst-interface-declaration-conc2
              • Cst-interface-declaration-conc1-rep
              • Cst-interface-declaration-conc1
              • Cst-integer-literal-conc4-rep-elem
              • Cst-integer-literal-conc3-rep-elem
              • Cst-integer-literal-conc1-rep-elem
              • Cst-import-declaration-conc4-rep-elem
              • Cst-import-declaration-conc4-rep
              • Cst-import-declaration-conc3-rep-elem
              • Cst-import-declaration-conc3-rep
              • Cst-import-declaration-conc2-rep-elem
              • Cst-import-declaration-conc2-rep
              • Cst-import-declaration-conc1-rep-elem
              • Cst-import-declaration-conc1-rep
              • Cst-hex-digits-and-underscores-conc
              • Cst-floating-point-literal-conc2
              • Cst-floating-point-literal-conc1
              • Cst-enum-constant-modifier-conc-rep-elem
              • Cst-compilation-unit-conc2-rep-elem
              • Cst-compilation-unit-conc1-rep-elem
              • Cst-compilation-unit-conc1-rep
              • Cst-class-or-interface-type-conc2
              • Cst-class-or-interface-type-conc1
              • Cst-class-declaration-conc2-rep-elem
              • Cst-class-declaration-conc1-rep-elem
              • Cst-class-body-declaration-conc4-rep
              • Cst-class-body-declaration-conc4
              • Cst-class-body-declaration-conc3-rep
              • Cst-class-body-declaration-conc3
              • Cst-class-body-declaration-conc2-rep
              • Cst-class-body-declaration-conc2
              • Cst-class-body-declaration-conc1-rep
              • Cst-class-body-declaration-conc1
              • Cst-block-statement-conc1-rep-elem
              • Cst-binary-exponent-indicator-conc-rep-elem
              • Cst-binary-exponent-indicator-conc-rep
              • Cst-binary-digits-and-underscores-conc
              • Cst-assignment-expression-conc2-rep
              • Cst-assignment-expression-conc2
              • Cst-assignment-expression-conc1-rep
              • Cst-assignment-expression-conc1
              • Cst-annotation-type-declaration-conc
              • Cst-variable-initializer-list-conc
              • Cst-variable-initializer-conc2
              • Cst-variable-initializer-conc1
              • Cst-variable-declarator-list-conc
              • Cst-variable-arity-parameter-conc
              • Cst-variable-access-conc2-rep-elem
              • Cst-variable-access-conc2-rep
              • Cst-variable-access-conc1-rep-elem
              • Cst-variable-access-conc1-rep
              • Cst-unann-type-variable-conc-rep-elem
              • Cst-unann-type-variable-conc-rep
              • Cst-unann-type-conc2-rep-elem
              • Cst-unann-type-conc1-rep-elem
              • Cst-unann-reference-type-conc3
              • Cst-unann-reference-type-conc2
              • Cst-unann-interface-type-conc-rep-elem
              • Cst-unann-interface-type-conc-rep
              • Cst-type-parameter-modifier-conc-rep
              • Cst-type-parameter-modifier-conc
              • Cst-type-argument-conc2-rep-elem
              • Cst-type-argument-conc2-rep
              • Cst-type-argument-conc1-rep-elem
              • Cst-type-argument-conc1-rep
              • Cst-synchronized-statement-conc
              • Cst-string-character-conc2-rep
              • Cst-string-character-conc2
              • Cst-string-character-conc1-rep
              • Cst-string-character-conc1
              • Cst-statement-expression-list-conc
              • Cst-statement-expression-conc6
              • Cst-statement-expression-conc1
              • Cst-single-element-annotation-conc
              • Cst-resource-specification-conc
              • Cst-reference-type-conc3-rep-elem
              • Cst-reference-type-conc3-rep
              • Cst-reference-type-conc2-rep-elem
              • Cst-reference-type-conc2-rep
              • Cst-reference-type-conc1-rep-elem
              • Cst-reference-type-conc1-rep
              • Cst-raw-input-character-conc-rep-elem
              • Cst-pre-increment-expression-conc
              • Cst-pre-decrement-expression-conc
              • Cst-postfix-expression-conc4
              • Cst-postfix-expression-conc3
              • Cst-postfix-expression-conc2
              • Cst-postfix-expression-conc1
              • Cst-post-increment-expression-conc
              • Cst-post-decrement-expression-conc
              • Cst-ordinary-compilation-unit-conc
              • Cst-numeric-type-conc2-rep-elem
              • Cst-numeric-type-conc1-rep-elem
              • Cst-not-star-not-slash-conc2
              • Cst-not-star-not-slash-conc1
              • Cst-normal-class-declaration-conc
              • Cst-modular-compilation-unit-conc
              • Cst-left-hand-side-conc3-rep-elem
              • Cst-left-hand-side-conc3-rep
              • Cst-left-hand-side-conc2-rep-elem
              • Cst-left-hand-side-conc2-rep
              • Cst-left-hand-side-conc1-rep-elem
              • Cst-left-hand-side-conc1-rep
              • Cst-lambda-body-conc2-rep-elem
              • Cst-lambda-body-conc1-rep-elem
              • Cst-java-letter-or-digit-conc-rep-elem
              • Cst-java-letter-or-digit-conc-rep
              • Cst-integer-type-suffix-conc-rep-elem
              • Cst-integer-literal-conc4-rep
              • Cst-integer-literal-conc4
              • Cst-integer-literal-conc3-rep
              • Cst-integer-literal-conc2-rep-elem
              • Cst-integer-literal-conc2-rep
              • Cst-integer-literal-conc1-rep
              • Cst-integer-literal-conc1
              • Cst-instance-initializer-conc-rep-elem
              • Cst-instance-initializer-conc-rep
              • Cst-input-element-conc3-rep-elem
              • Cst-input-element-conc3-rep
              • Cst-input-element-conc2-rep-elem
              • Cst-input-element-conc2-rep
              • Cst-input-element-conc1-rep-elem
              • Cst-input-element-conc1-rep
              • Cst-import-declaration-conc4
              • Cst-import-declaration-conc3
              • Cst-import-declaration-conc2
              • Cst-import-declaration-conc1
              • Cst-if-then-else-statement-conc
              • Cst-for-statement-conc2-rep-elem
              • Cst-for-statement-conc2-rep
              • Cst-for-statement-conc1-rep-elem
              • Cst-for-statement-conc1-rep
              • Cst-expression-conc2-rep-elem
              • Cst-expression-conc1-rep-elem
              • Cst-exponent-indicator-conc-rep-elem
              • Cst-exception-type-conc2-rep-elem
              • Cst-exception-type-conc2-rep
              • Cst-exception-type-conc1-rep-elem
              • Cst-exception-type-conc1-rep
              • Cst-enum-constant-modifier-conc-rep
              • Cst-enum-body-declarations-conc
              • Cst-enhanced-for-statement-conc
              • Cst-element-value-pair-list-conc
              • Cst-element-value-conc3-rep-elem
              • Cst-element-value-conc3-rep
              • Cst-element-value-conc2-rep-elem
              • Cst-element-value-conc2-rep
              • Cst-element-value-conc1-rep-elem
              • Cst-element-value-conc1-rep
              • Cst-digits-and-underscores-conc
              • Cst-decimal-integer-literal-conc
              • Cst-constructor-declarator-conc
              • Cst-constructor-declaration-conc
              • Cst-constant-expression-conc-rep-elem
              • Cst-compilation-unit-conc2-rep
              • Cst-compilation-unit-conc2
              • Cst-compilation-unit-conc1
              • Cst-class-declaration-conc2-rep
              • Cst-class-declaration-conc2
              • Cst-class-declaration-conc1-rep
              • Cst-class-declaration-conc1
              • Cst-catch-formal-parameter-conc
              • Cst-block-statement-conc3-rep-elem
              • Cst-block-statement-conc3-rep
              • Cst-block-statement-conc2-rep-elem
              • Cst-block-statement-conc2-rep
              • Cst-block-statement-conc1-rep
              • Cst-block-statement-conc1
              • Cst-binary-integer-literal-conc
              • Cst-binary-exponent-indicator-conc
              • Cst-annotation-conc3-rep-elem
              • Cst-annotation-conc2-rep-elem
              • Cst-annotation-conc1-rep-elem
              • Abnf-tree-list-with-root-p
              • Cst-variable-declarator-id-conc
              • Cst-variable-declarator-conc
              • Cst-variable-access-conc2
              • Cst-variable-access-conc1
              • Cst-unann-type-variable-conc
              • Cst-unann-type-conc2-rep
              • Cst-unann-type-conc1-rep
              • Cst-unann-interface-type-conc
              • Cst-type-parameter-list-conc
              • Cst-type-identifier-conc-rep-elem
              • Cst-type-identifier-conc-rep
              • Cst-type-argument-list-conc
              • Cst-type-argument-conc2
              • Cst-type-argument-conc1
              • Cst-traditional-comment-conc
              • Cst-switch-expression-conc
              • Cst-static-initializer-conc
              • Cst-statement-conc6-rep-elem
              • Cst-statement-conc6-rep
              • Cst-statement-conc5-rep-elem
              • Cst-statement-conc5-rep
              • Cst-statement-conc4-rep-elem
              • Cst-statement-conc4-rep
              • Cst-statement-conc3-rep-elem
              • Cst-statement-conc3-rep
              • Cst-statement-conc2-rep-elem
              • Cst-statement-conc2-rep
              • Cst-statement-conc1-rep-elem
              • Cst-statement-conc1-rep
              • Cst-single-character-conc-rep-elem
              • Cst-single-character-conc-rep
              • Cst-simple-type-name-conc-rep-elem
              • Cst-simple-type-name-conc-rep
              • Cst-reference-type-conc3
              • Cst-reference-type-conc2
              • Cst-reference-type-conc1
              • Cst-receiver-parameter-conc
              • Cst-raw-input-character-conc-rep
              • Cst-raw-input-character-conc
              • Cst-primary-conc2-rep-elem
              • Cst-primary-conc1-rep-elem
              • Cst-package-modifier-conc-rep-elem
              • Cst-package-modifier-conc-rep
              • Cst-package-declaration-conc
              • Cst-octal-integer-literal-conc
              • Cst-numeric-type-conc2-rep
              • Cst-numeric-type-conc2
              • Cst-numeric-type-conc1-rep
              • Cst-numeric-type-conc1
              • Cst-null-literal-conc-rep-elem
              • Cst-not-star-conc2-rep-elem
              • Cst-not-star-conc1-rep-elem
              • Cst-normal-annotation-conc
              • Cst-module-declaration-conc
              • Cst-method-name-conc-rep-elem
              • Cst-method-declarator-conc
              • Cst-method-declaration-conc
              • Cst-literal-conc6-rep-elem
              • Cst-literal-conc5-rep-elem
              • Cst-literal-conc4-rep-elem
              • Cst-literal-conc3-rep-elem
              • Cst-literal-conc2-rep-elem
              • Cst-literal-conc1-rep-elem
              • Cst-left-hand-side-conc3
              • Cst-left-hand-side-conc2
              • Cst-left-hand-side-conc1
              • Cst-lambda-expression-conc
              • Cst-lambda-body-conc2-rep
              • Cst-lambda-body-conc2
              • Cst-lambda-body-conc1-rep
              • Cst-lambda-body-conc1
              • Cst-labeled-statement-conc
              • Cst-java-letter-or-digit-conc
              • Cst-interface-type-list-conc
              • Cst-interface-type-conc-rep-elem
              • Cst-integer-type-suffix-conc-rep
              • Cst-integer-type-suffix-conc
              • Cst-integer-literal-conc3
              • Cst-integer-literal-conc2
              • Cst-instance-initializer-conc
              • Cst-input-element-conc3
              • Cst-input-element-conc2
              • Cst-input-element-conc1
              • Cst-input-character-conc-rep-elem
              • Cst-input-character-conc-rep
              • Cst-if-then-statement-conc
              • Cst-hex-integer-literal-conc
              • Cst-formal-parameter-list-conc
              • Cst-for-statement-conc2
              • Cst-for-statement-conc1
              • Cst-for-init-conc2-rep-elem
              • Cst-for-init-conc2-rep
              • Cst-for-init-conc1-rep-elem
              • Cst-for-init-conc1-rep
              • Cst-field-declaration-conc
              • Cst-extends-interfaces-conc
              • Cst-expression-statement-conc
              • Cst-expression-conc2-rep
              • Cst-expression-conc1-rep
              • Cst-exponent-indicator-conc-rep
              • Cst-exponent-indicator-conc
              • Cst-exception-type-list-conc
              • Cst-exception-type-conc2
              • Cst-exception-type-conc1
              • Cst-enum-constant-modifier-conc
              • Cst-enum-constant-list-conc
              • Cst-end-of-line-comment-conc
              • Cst-empty-statement-conc-rep-elem
              • Cst-empty-statement-conc-rep
              • Cst-element-value-pair-conc
              • Cst-element-value-list-conc
              • Cst-element-value-conc3
              • Cst-element-value-conc2
              • Cst-element-value-conc1
              • Cst-continue-statement-conc
              • Cst-constant-expression-conc-rep
              • Cst-constant-expression-conc
              • Cst-constant-declaration-conc
              • Cst-comment-conc2-rep-elem
              • Cst-comment-conc1-rep-elem
              • Cst-case-constant-conc-rep-elem
              • Cst-block-statement-conc3
              • Cst-block-statement-conc2
              • Cst-basic-for-statement-conc
              • Cst-array-initializer-conc
              • Cst-annotation-type-body-conc
              • Cst-annotation-conc3-rep
              • Cst-annotation-conc3
              • Cst-annotation-conc2-rep
              • Cst-annotation-conc1-rep
              • Cst-yield-statement-conc
              • Cst-while-statement-conc
              • Cst-unicode-marker-conc
              • Cst-unicode-escape-conc
              • Cst-unann-type-conc2
              • Cst-unann-type-conc1
              • Cst-type-variable-conc
              • Cst-type-parameters-conc
              • Cst-type-parameter-conc
              • Cst-type-identifier-conc
              • Cst-type-conc2-rep-elem
              • Cst-type-conc1-rep-elem
              • Cst-type-arguments-conc
              • Cst-token-conc5-rep-elem
              • Cst-token-conc4-rep-elem
              • Cst-token-conc3-rep-elem
              • Cst-token-conc2-rep-elem
              • Cst-token-conc1-rep-elem
              • Cst-throw-statement-conc
              • Cst-switch-statement-conc
              • Cst-superinterfaces-conc
              • Cst-string-literal-conc
              • Cst-statement-conc6
              • Cst-statement-conc5
              • Cst-statement-conc4
              • Cst-statement-conc3
              • Cst-statement-conc2
              • Cst-statement-conc1
              • Cst-single-character-conc
              • Cst-simple-type-name-conc
              • Cst-signed-integer-conc
              • Cst-return-statement-conc
              • Cst-resource-list-conc
              • Cst-primary-conc2-rep
              • Cst-primary-conc2
              • Cst-primary-conc1-rep
              • Cst-primary-conc1
              • Cst-package-modifier-conc
              • Cst-null-literal-conc-rep
              • Cst-not-star-conc2-rep
              • Cst-not-star-conc2
              • Cst-not-star-conc1-rep
              • Cst-not-star-conc1
              • Cst-method-name-conc-rep
              • Cst-marker-annotation-conc
              • Cst-literal-conc6-rep
              • Cst-literal-conc6
              • Cst-literal-conc5-rep
              • Cst-literal-conc5
              • Cst-literal-conc4-rep
              • Cst-literal-conc4
              • Cst-literal-conc3-rep
              • Cst-literal-conc3
              • Cst-literal-conc2-rep
              • Cst-literal-conc2
              • Cst-literal-conc1-rep
              • Cst-literal-conc1
              • Cst-java-letter-conc-rep-elem
              • Cst-java-letter-conc-rep
              • Cst-interface-type-conc-rep
              • Cst-interface-type-conc
              • Cst-interface-body-conc
              • Cst-input-character-conc
              • Cst-identifier-conc-rep-elem
              • Cst-identifier-chars-conc
              • Cst-for-update-conc-rep-elem
              • Cst-for-update-conc-rep
              • Cst-for-init-conc2
              • Cst-for-init-conc1
              • Cst-expression-conc2
              • Cst-expression-conc1
              • Cst-exponent-part-conc
              • Cst-enum-declaration-conc
              • Cst-enum-constant-conc
              • Cst-empty-statement-conc
              • Cst-do-statement-conc
              • Cst-default-value-conc
              • Cst-constructor-body-conc
              • Cst-comment-conc2-rep
              • Cst-comment-conc2
              • Cst-comment-conc1-rep
              • Cst-comment-conc1
              • Cst-catch-clause-conc
              • Cst-case-constant-conc-rep
              • Cst-case-constant-conc
              • Cst-break-statement-conc
              • Cst-block-statements-conc
              • Cst-binary-numeral-conc
              • Cst-binary-exponent-conc
              • Cst-argument-list-conc
              • Cst-annotation-conc2
              • Cst-annotation-conc1
              • Cst-additional-bound-conc
              • Cst-wildcard-conc
              • Cst-underscores-conc
              • Cst-type-conc2-rep
              • Cst-type-conc2
              • Cst-type-conc1-rep
              • Cst-type-conc1
              • Cst-token-conc5-rep
              • Cst-token-conc5
              • Cst-token-conc4-rep
              • Cst-token-conc4
              • Cst-token-conc3-rep
              • Cst-token-conc3
              • Cst-token-conc2-rep
              • Cst-token-conc2
              • Cst-token-conc1-rep
              • Cst-token-conc1
              • Cst-superclass-conc
              • Cst-sub-conc-rep-elem
              • Cst-null-literal-conc
              • Cst-method-name-conc
              • Cst-java-letter-conc
              • Cst-identifier-conc-rep
              • Cst-identifier-conc
              • Cst-hex-numeral-conc
              • Cst-for-update-conc
              • Cst-enum-body-conc
              • Cst-dim-exprs-conc
              • Cst-dim-expr-conc
              • Cst-class-body-conc
              • Cst-catch-type-conc
              • Cst-assignment-conc
              • Cst-throws-conc
              • Cst-sub-conc-rep
              • Cst-sub-conc
              • Cst-input-conc
              • Cst-finally-conc
              • Cst-dims-conc
              • Cst-catches-conc
              • Cst-block-conc
              • Cst-%x0-ffff-nat
              • *syntactic-grammar*
              • *lexical-grammar*
            • Unicode-escapes
            • Unicode-input-char
            • Escape-sequence
            • Identifiers
            • Primitive-types
            • Reference-types
            • Keywords
            • Unicode-characters
            • Integer-literals
            • String-literals
            • Octal-digits
            • Hexadecimal-digits
            • Decimal-digits
            • Binary-digits
            • Character-literals
            • Null-literal
            • Floating-point-literals
            • Boolean-literals
            • Package-names
            • Literals
          • Semantics
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Grammar

*syntactic-grammar*

The Java syntactic grammar, in ABNF.

We parse the grammar file to obtain an ABNF grammar value.

Definitions and Theorems

Function: untranslate-preprocess-*syntactic-grammar*

(defun untranslate-preprocess-*syntactic-grammar*
       (acl2::term acl2::wrld)
 (if (equal acl2::term
            (list 'quote *syntactic-grammar*))
     '*syntactic-grammar*
  (untranslate-preprocess-*lexical-grammar* acl2::term acl2::wrld)))

Theorem: rulelist-wfp-of-*syntactic-grammar*

(defthm rulelist-wfp-of-*syntactic-grammar*
  (abnf::rulelist-wfp *syntactic-grammar*))