meta-language 1.0.0

(grammar (start source_file) (matching longest) (settling tokens precedence dynamic ambiguity))
(extra (class plain (char %20) (char %09) (char %0A) (char %0D) (char %0C) (char %0B)))
(extra (ref comment))
(conflict generic_tactic_body)
(conflict match_pattern list_literal)
(conflict binder)
(conflict fixpoint_annotation qualified_identifier)
(conflict assert_tactic qualified_identifier)
(conflict hundred_level_term term_cast)
(conflict name annotated_qualified_identifier)
(conflict local_definition qualified_identifier)
(conflict generic_tactic)
(conflict field_definition annotated_qualified_identifier)
(conflict one_term ten_level_pattern)
(conflict rewrite_term list_literal)
(conflict list_literal list_pattern)
(conflict zero_level_term pattern)
(conflict zero_level_pattern annotated_qualified_identifier)
(conflict zero_level_term zero_level_pattern)
(precedences (name scope) (name application) (name negation) (name list_ops) (name multiplicative) (name additive) (name comparison) (name conjunction) (name disjunction) (name equivalence) (name custom) (name arrow_term) (name quantifier_term) (name binder) (name type))
(precedences (name tactic_match) (name tactic_application) (name tactic_or) (name tactic_sequence) (name tactic_let))
(rule source_file normal (repeat0 (ref sentence)) (concept grammar.source-file))
(rule sentence normal (choice unordered (seq (optional (ref fail_prefix)) (optional (ref attributes)) (optional (ref selector)) (choice unordered (ref vernacular_command) (ref ltac_definition) (ref ltac_expression)) (choice unordered (literal .) (literal ...))) (ref proof_block) (ref bullet)) (concept grammar.sentence))
(rule fail_prefix token (seq (literal Fail) (not (ref word_characters))) (concept grammar.fail-prefix) (source-names (tree-sitter fail)))
(rule attributes normal (choice unordered (seq (repeat1 (ref modern_attribute_block)) (repeat0 (ref legacy_attribute))) (repeat1 (ref legacy_attribute))) (concept grammar.attribute-list))
(rule modern_attribute_block silent (seq (literal %23) (literal %5B) (optional (seq (ref attribute) (repeat0 (seq (literal %2C) (ref attribute))))) (literal %5D)) (concept grammar.modern-attribute-block) (source-names (tree-sitter _modern_attribute_block)))
(rule attribute normal (seq (ref identifier) (optional (ref attribute_value))) (concept program.attributes))
(rule attribute_value normal (choice unordered (seq (literal %3D) (ref string)) (seq (literal %3D) (ref qualified_identifier)) (seq (literal %28) (ref attribute) (repeat0 (seq (literal %2C) (ref attribute))) (literal %29))) (concept grammar.attribute-value) (source-names (tree-sitter attr_value)))
(rule legacy_attribute normal (choice unordered (choice unordered (token (seq (literal Local) (not (ref word_characters)))) (token (seq (literal Global) (not (ref word_characters))))) (choice unordered (token (seq (literal Polymorphic) (not (ref word_characters)))) (token (seq (literal Monomorphic) (not (ref word_characters))))) (choice unordered (token (seq (literal Cumulative) (not (ref word_characters)))) (token (seq (literal NonCumulative) (not (ref word_characters))))) (token (seq (literal Private) (not (ref word_characters)))) (token (seq (literal Program) (not (ref word_characters))))) (concept grammar.legacy-attribute) (source-names (tree-sitter legacy_attr)))
(rule selector normal (seq (choice unordered (ref goal_selector) (token (seq (literal all) (not (ref word_characters)))) (literal %21) (token (seq (literal par) (not (ref word_characters))))) (literal %3A)) (concept grammar.selector))
(rule goal_selector normal (seq (ref range_selector) (repeat0 (seq (literal %2C) (ref range_selector)))) (concept grammar.goal-selector))
(rule range_selector normal (choice unordered (ref natural) (seq (literal %5B) (ref qualified_identifier) (literal %5D)) (seq (capture labeled start (ref natural)) (literal -) (capture labeled end (ref natural)))) (concept grammar.range-selector))
(rule vernacular_command silent (choice unordered (ref require_command) (ref import_command) (ref export_command) (ref create_hint_database_command) (ref create_rewrite_hint_database_command) (ref hint_command) (ref evaluation_command) (ref extraction_command) (ref extract_command) (ref set_command) (ref unset_command) (ref add_command) (ref remove_command) (ref test_command) (ref show_proof_command) (ref coercion_command) (ref declare_command) (ref open_scope_command) (ref close_scope_command) (ref theorem_command) (ref definition_command) (ref fixpoint_command) (ref function_command) (ref inductive_command) (ref assumption_command) (ref arguments_command) (ref section_command) (ref module_command) (ref end_command) (ref reserved_notation_command) (ref notation_command) (ref infix_command) (ref abbreviation_command) (ref include_command) (ref register_command) (ref instance_command) (ref existing_command) (ref record_command) (ref scheme_command) (ref combined_scheme_command) (ref delimit_scope_command) (ref bind_scope_command) (ref context_command) (ref obligation_tactic_command) (ref obligation_command) (ref implicit_types_command) (ref type_classes_command) (ref generalizable_command) (ref proof_command) (ref qed_command) (ref save_command) (ref defined_command) (ref admitted_command) (ref abort_command)) (concept grammar.vernacular-command) (source-names (tree-sitter _vernacular_command)))
(rule require_command normal (seq (optional (seq (token (seq (literal From) (not (ref word_characters)))) (capture labeled dirpath (ref qualified_identifier)))) (token (seq (literal Require) (not (ref word_characters)))) (optional (seq (choice unordered (token (seq (literal Import) (not (ref word_characters)))) (token (seq (literal Export) (not (ref word_characters))))) (optional (ref import_categories)))) (repeat1 (ref filtered_import))) (concept grammar.require-command))
(rule import_command normal (seq (token (seq (literal Import) (not (ref word_characters)))) (optional (ref import_categories)) (repeat1 (ref filtered_import))) (concept grammar.import-statement))
(rule export_command normal (seq (token (seq (literal Export) (not (ref word_characters)))) (optional (ref import_categories)) (repeat1 (ref filtered_import))) (concept grammar.export-statement))
(rule negated_selection normal (literal -) (concept grammar.negated-selection) (source-names (tree-sitter neg_selection)))
(rule import_categories normal (seq (optional (ref negated_selection)) (literal %28) (capture labeled category (ref qualified_identifier)) (repeat0 (seq (literal %2C) (capture labeled category (ref qualified_identifier)))) (literal %29)) (concept grammar.import-categories))
(rule filtered_import normal (seq (capture labeled module (ref qualified_identifier)) (optional (seq (literal %28) (ref filtered_import_item) (repeat0 (seq (literal %2C) (ref filtered_import_item))) (literal %29)))) (concept grammar.filtered-import))
(rule filtered_import_item normal (seq (capture labeled name (ref qualified_identifier)) (optional (ref import_wildcard))) (concept grammar.filtered-import-item))
(rule import_wildcard token (literal %28..%29) (concept grammar.import-wildcard))
(rule create_hint_database_command normal (seq (token (seq (literal Create) (not (ref word_characters)))) (token (seq (literal HintDb) (not (ref word_characters)))) (capture labeled name (ref identifier)) (optional (ref discriminated_database))) (concept grammar.create-hint-database-command) (source-names (tree-sitter create_hintdb_command)))
(rule create_rewrite_hint_database_command normal (seq (token (seq (literal Create) (not (ref word_characters)))) (token (seq (literal Rewrite) (not (ref word_characters)))) (token (seq (literal HintDb) (not (ref word_characters)))) (capture labeled name (ref identifier))) (concept grammar.create-rewrite-hint-database-command) (source-names (tree-sitter create_rewrite_hintdb_command)))
(rule discriminated_database token (seq (literal discriminated) (not (ref word_characters))) (concept grammar.discriminated-database) (source-names (tree-sitter discriminated_db)))
(rule hint_command normal (seq (token (seq (literal Hint) (not (ref word_characters)))) (choice unordered (ref hint_extern) (seq (choice unordered (token (seq (literal Resolve) (not (ref word_characters)))) (token (seq (literal Rewrite) (not (ref word_characters)))) (token (seq (literal Constructors) (not (ref word_characters)))) (token (seq (literal Unfold) (not (ref word_characters)))) (token (seq (literal Immediate) (not (ref word_characters)))) (token (seq (literal Transparent) (not (ref word_characters)))) (token (seq (literal Opaque) (not (ref word_characters))))) (optional (choice unordered (literal -%3E) (literal %3C-))) (repeat1 (capture labeled name (ref one_term))) (optional (ref hint_priority)) (optional (seq (literal %3A) (repeat1 (capture labeled database (ref identifier)))))) (seq (choice unordered (token (seq (literal Variables) (not (ref word_characters)))) (token (seq (literal Constants) (not (ref word_characters)))) (token (seq (literal Projections) (not (ref word_characters))))) (choice unordered (token (seq (literal Opaque) (not (ref word_characters)))) (token (seq (literal Transparent) (not (ref word_characters))))) (optional (seq (literal %3A) (repeat1 (capture labeled database (ref identifier)))))) (seq (token (seq (literal Mode) (not (ref word_characters)))) (ref qualified_identifier) (repeat1 (choice unordered (literal %2B) (literal -) (literal %21))) (optional (seq (literal %3A) (repeat1 (capture labeled database (ref identifier)))))) (seq (token (seq (literal Cut) (not (ref word_characters)))) (literal %5B) (repeat0 (choice unordered (ref qualified_identifier) (literal %7C) (literal %2A) (literal %28) (literal %29) (token (seq (literal _) (not (ref word_characters)))))) (literal %5D) (optional (seq (literal %3A) (repeat1 (capture labeled database (ref identifier)))))))) (concept grammar.hint-command))
(rule hint_extern normal (seq (token (seq (literal Extern) (not (ref word_characters)))) (capture labeled cost (ref natural)) (capture labeled pattern (optional (ref one_pattern))) (literal %3D%3E) (capture labeled tactic (ref ltac_expression)) (optional (seq (literal %3A) (repeat1 (capture labeled database (ref identifier)))))) (concept grammar.hint-extern))
(rule one_pattern silent (ref one_term) (concept grammar.one-pattern) (source-names (tree-sitter _one_pattern)))
(rule evaluation_command normal (choice unordered (seq (choice unordered (token (seq (literal Check) (not (ref word_characters)))) (token (seq (literal Compute) (not (ref word_characters)))) (token (seq (literal Print) (not (ref word_characters)))) (token (seq (literal Search) (not (ref word_characters)))) (token (seq (literal Locate) (not (ref word_characters)))) (token (seq (literal About) (not (ref word_characters))))) (ref term)) (seq (token (seq (literal Eval) (not (ref word_characters)))) (ref reduction_expression) (token (seq (literal in) (not (ref word_characters)))) (ref term))) (concept grammar.evaluation-command))
(rule reduction_expression normal (seq (ref identifier) (repeat0 (choice unordered (ref identifier) (seq (optional (literal -)) (literal %5B) (repeat0 (ref global_reference)) (literal %5D))))) (concept grammar.reduction-expression) (source-names (tree-sitter reduction_expr)))
(rule extraction_command normal (choice unordered (seq (token (seq (literal Extraction) (not (ref word_characters)))) (ref qualified_identifier)) (seq (token (seq (literal Recursive) (not (ref word_characters)))) (token (seq (literal Extraction) (not (ref word_characters)))) (repeat1 (ref qualified_identifier))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (ref string) (repeat1 (ref qualified_identifier))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal Library) (not (ref word_characters)))) (ref identifier)) (seq (token (seq (literal Recursive) (not (ref word_characters)))) (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal Library) (not (ref word_characters)))) (ref identifier)) (seq (token (seq (literal Separete) (not (ref word_characters)))) (token (seq (literal Extraction) (not (ref word_characters)))) (repeat1 (ref qualified_identifier))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal TestCompile) (not (ref word_characters)))) (repeat1 (ref qualified_identifier))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal Language) (not (ref word_characters)))) (ref language)) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal Optimize) (not (ref word_characters))))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal Conservative) (not (ref word_characters)))) (token (seq (literal Types) (not (ref word_characters))))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal KeepSingleton) (not (ref word_characters))))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal AutoInline) (not (ref word_characters))))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (choice unordered (token (seq (literal Inline) (not (ref word_characters)))) (token (seq (literal NoInline) (not (ref word_characters))))) (repeat1 (ref qualified_identifier))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal Implicit) (not (ref word_characters)))) (ref qualified_identifier) (literal %5B) (repeat0 (choice unordered (ref identifier) (ref integer))) (literal %5D)) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal SafeImplicits) (not (ref word_characters))))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal AccessOpaque) (not (ref word_characters))))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal Blacklist) (not (ref word_characters)))) (repeat1 (ref identifier))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal File) (not (ref word_characters)))) (token (seq (literal Comment) (not (ref word_characters)))) (ref string)) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal Flag) (not (ref word_characters)))) (ref natural)) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal TypeExpand) (not (ref word_characters))))) (seq (token (seq (literal Extraction) (not (ref word_characters)))) (token (seq (literal Output) (not (ref word_characters)))) (token (seq (literal Directory) (not (ref word_characters)))) (ref string))) (concept grammar.extraction-command))
(rule extract_command normal (choice unordered (seq (token (seq (literal Extract) (not (ref word_characters)))) (token (seq (literal Constant) (not (ref word_characters)))) (ref qualified_identifier) (repeat0 (ref string)) (literal %3D%3E) (choice unordered (ref identifier) (ref string))) (seq (token (seq (literal Extract) (not (ref word_characters)))) (token (seq (literal Inlined) (not (ref word_characters)))) (token (seq (literal Constant) (not (ref word_characters)))) (ref qualified_identifier) (literal %3D%3E) (choice unordered (ref identifier) (ref string))) (seq (token (seq (literal Extract) (not (ref word_characters)))) (token (seq (literal Inductive) (not (ref word_characters)))) (ref qualified_identifier) (literal %3D%3E) (choice unordered (ref identifier) (ref string)) (literal %5B) (repeat0 (choice unordered (ref identifier) (ref string))) (literal %5D) (optional (ref string))) (seq (token (seq (literal Extract) (not (ref word_characters)))) (token (seq (literal Foreign) (not (ref word_characters)))) (token (seq (literal Constant) (not (ref word_characters)))) (ref qualified_identifier) (literal %3D%3E) (ref string)) (seq (token (seq (literal Extract) (not (ref word_characters)))) (token (seq (literal Callback) (not (ref word_characters)))) (optional (ref string)) (ref qualified_identifier))) (concept grammar.extract-command))
(rule language normal (choice unordered (token (seq (literal OCaml) (not (ref word_characters)))) (token (seq (literal Haskell) (not (ref word_characters)))) (token (seq (literal Scheme) (not (ref word_characters)))) (token (seq (literal JSON) (not (ref word_characters))))) (concept grammar.language))
(rule set_command normal (seq (token (seq (literal Set) (not (ref word_characters)))) (ref setting_name) (optional (choice unordered (ref integer) (ref string)))) (concept grammar.set-command))
(rule unset_command normal (seq (token (seq (literal Unset) (not (ref word_characters)))) (ref setting_name)) (concept grammar.unset-command))
(rule add_command normal (choice unordered (seq (token (seq (literal Add) (not (ref word_characters)))) (token (seq (literal Printing) (not (ref word_characters)))) (choice unordered (token (seq (literal If) (not (ref word_characters)))) (token (seq (literal Let) (not (ref word_characters)))) (token (seq (literal Record) (not (ref word_characters)))) (token (seq (literal Constructor) (not (ref word_characters))))) (repeat1 (ref qualified_identifier))) (seq (token (seq (literal Add) (not (ref word_characters)))) (ref setting_name) (repeat1 (choice unordered (ref qualified_identifier) (ref string))))) (concept grammar.add-command))
(rule remove_command normal (choice unordered (seq (token (seq (literal Remove) (not (ref word_characters)))) (token (seq (literal Printing) (not (ref word_characters)))) (choice unordered (token (seq (literal If) (not (ref word_characters)))) (token (seq (literal Let) (not (ref word_characters)))) (token (seq (literal Record) (not (ref word_characters)))) (token (seq (literal Constructor) (not (ref word_characters))))) (repeat1 (ref qualified_identifier))) (seq (token (seq (literal Remove) (not (ref word_characters)))) (token (seq (literal Hints) (not (ref word_characters)))) (repeat1 (ref qualified_identifier)) (optional (seq (literal %3A) (repeat1 (ref identifier))))) (seq (token (seq (literal Remove) (not (ref word_characters)))) (ref setting_name) (repeat1 (choice unordered (ref qualified_identifier) (ref string))))) (concept grammar.remove-command))
(rule test_command normal (seq (token (seq (literal Test) (not (ref word_characters)))) (ref setting_name) (optional (seq (token (seq (literal for) (not (ref word_characters)))) (repeat1 (choice unordered (ref qualified_identifier) (ref string)))))) (concept grammar.test-command))
(rule setting_name normal (precedence 0 right (repeat1 (ref identifier))) (concept grammar.setting-name))
(rule show_proof_command normal (seq (token (seq (literal Show) (not (ref word_characters)))) (token (seq (literal Proof) (not (ref word_characters)))) (optional (seq (token (seq (literal Diffs) (not (ref word_characters)))) (optional (token (seq (literal removed) (not (ref word_characters)))))))) (concept grammar.show-proof-command))
(rule coercion_command normal (seq (token (seq (literal Coercion) (not (ref word_characters)))) (capture labeled name (ref global_reference)) (optional (seq (literal %3A) (ref coercion_class) (literal %3E-%3E) (ref coercion_class)))) (concept grammar.coercion-command))
(rule coercion_class normal (choice unordered (token (seq (literal Funclass) (not (ref word_characters)))) (token (seq (literal Sortclass) (not (ref word_characters)))) (ref global_reference)) (concept grammar.coercion-class))
(rule declare_command normal (choice unordered (seq (token (seq (literal Declare) (not (ref word_characters)))) (token (seq (literal Module) (not (ref word_characters)))) (optional (choice unordered (token (seq (literal Import) (not (ref word_characters)))) (token (seq (literal Export) (not (ref word_characters)))))) (capture labeled name (ref identifier)) (repeat0 (ref module_binder)) (literal %3A) (ref module_type_expression)) (seq (token (seq (literal Declare) (not (ref word_characters)))) (token (seq (literal Reduction) (not (ref word_characters)))) (ref identifier) (literal %3A%3D) (ref identifier) (repeat0 (ref qualified_identifier))) (seq (token (seq (literal Declare) (not (ref word_characters)))) (choice unordered (token (seq (literal Left) (not (ref word_characters)))) (token (seq (literal Right) (not (ref word_characters))))) (token (seq (literal Step) (not (ref word_characters)))) (ref qualified_identifier)) (ref declare_scope_command) (ref declare_custom_entry_command)) (concept grammar.declare-command))
(rule declare_scope_command silent (seq (token (seq (literal Declare) (not (ref word_characters)))) (token (seq (literal Scope) (not (ref word_characters)))) (capture labeled name (ref identifier))) (concept grammar.declare-scope-command) (source-names (tree-sitter _declare_scope_command)))
(rule declare_custom_entry_command silent (seq (token (seq (literal Declare) (not (ref word_characters)))) (token (seq (literal Custom) (not (ref word_characters)))) (token (seq (literal Entry) (not (ref word_characters)))) (capture labeled name (ref identifier))) (concept grammar.declare-custom-entry-command) (source-names (tree-sitter _declare_custom_entry_command)))
(rule open_scope_command normal (seq (token (seq (literal Open) (not (ref word_characters)))) (token (seq (literal Scope) (not (ref word_characters)))) (capture labeled name (ref identifier))) (concept grammar.open-scope-command))
(rule close_scope_command normal (seq (token (seq (literal Close) (not (ref word_characters)))) (token (seq (literal Scope) (not (ref word_characters)))) (capture labeled name (ref identifier))) (concept grammar.close-scope-command))
(rule theorem_command normal (seq (choice unordered (token (seq (literal Theorem) (not (ref word_characters)))) (token (seq (literal Lemma) (not (ref word_characters)))) (token (seq (literal Fact) (not (ref word_characters)))) (token (seq (literal Remark) (not (ref word_characters)))) (token (seq (literal Corollary) (not (ref word_characters)))) (token (seq (literal Proposition) (not (ref word_characters)))) (token (seq (literal Property) (not (ref word_characters))))) (ref identifier_declaration) (repeat0 (ref binder)) (literal %3A) (ref type) (repeat0 (seq (token (seq (literal with) (not (ref word_characters)))) (ref identifier_declaration) (repeat0 (ref binder)) (literal %3A) (ref type)))) (concept grammar.theorem-command))
(rule definition_command normal (seq (choice unordered (token (seq (literal Definition) (not (ref word_characters)))) (token (seq (literal Example) (not (ref word_characters)))) (token (seq (literal Let) (not (ref word_characters))))) (ref identifier_declaration) (ref definition_body)) (concept grammar.definition-command))
(rule definition_body silent (choice unordered (seq (repeat0 (ref binder)) (optional (seq (literal %3A) (ref type))) (literal %3A%3D) (capture labeled body (ref term))) (seq (repeat0 (ref binder)) (literal %3A) (ref type))) (concept grammar.definition-body) (source-names (tree-sitter _def_body)))
(rule fixpoint_command normal (seq (token (seq (literal Fixpoint) (not (ref word_characters)))) (ref fix_definition) (repeat0 (seq (token (seq (literal with) (not (ref word_characters)))) (ref fix_definition)))) (concept grammar.fixpoint-command))
(rule function_command normal (seq (token (seq (literal Function) (not (ref word_characters)))) (ref fix_definition) (repeat0 (seq (token (seq (literal with) (not (ref word_characters)))) (ref fix_definition)))) (concept grammar.function-command))
(rule fix_definition silent (seq (ref identifier_declaration) (repeat0 (ref binder)) (optional (ref fixpoint_annotation)) (optional (seq (literal %3A) (ref type))) (optional (seq (literal %3A%3D) (capture labeled body (ref term)))) (optional (ref declaration_notations))) (concept grammar.fix-definition) (source-names (tree-sitter _fix_definition)))
(rule fixpoint_annotation normal (choice unordered (seq (literal %7B) (token (seq (literal struct) (not (ref word_characters)))) (ref identifier) (literal %7D)) (seq (literal %7B) (token (seq (literal wf) (not (ref word_characters)))) (ref one_term) (ref identifier) (literal %7D)) (seq (literal %7B) (token (seq (literal measure) (not (ref word_characters)))) (ref one_term) (optional (ref identifier)) (optional (ref one_term)) (literal %7D))) (concept grammar.fixpoint-annotation) (source-names (tree-sitter fixannot)))
(rule declaration_notations normal (seq (token (seq (literal where) (not (ref word_characters)))) (ref notation_declaration) (repeat0 (seq (token (seq (literal and) (not (ref word_characters)))) (ref notation_declaration)))) (concept grammar.declaration-notations) (source-names (tree-sitter decl_notations)))
(rule inductive_command normal (seq (choice unordered (token (seq (literal Inductive) (not (ref word_characters)))) (token (seq (literal CoInductive) (not (ref word_characters)))) (token (seq (literal Variant) (not (ref word_characters))))) (ref inductive_definition) (repeat0 (seq (token (seq (literal with) (not (ref word_characters)))) (ref inductive_definition)))) (concept grammar.inductive-command))
(rule inductive_definition normal (seq (capture labeled name (ref identifier)) (repeat0 (ref binder)) (optional (seq (literal %7C) (repeat0 (ref binder)))) (optional (seq (literal %3A) (ref type))) (literal %3A%3D) (optional (ref constructor_block)) (optional (ref declaration_notations))) (concept grammar.inductive-definition))
(rule constructor_block normal (seq (optional (literal %7C)) (ref constructor) (repeat0 (seq (literal %7C) (ref constructor)))) (concept grammar.constructor-block))
(rule constructor normal (seq (repeat0 (ref constructor_attribute)) (capture labeled name (ref identifier)) (repeat0 (ref binder)) (optional (ref of_type_instance))) (concept grammar.constructor))
(rule of_type_instance normal (seq (choice unordered (literal %3A) (literal %3A%3E) (literal %3A%3A) (literal %3A%3A%3E)) (ref type)) (concept grammar.of-type-instance) (source-names (tree-sitter of_type_inst)))
(rule constructor_attribute silent (seq (literal %23) (literal %5B) (ref attribute) (repeat0 (seq (literal %2C) (ref attribute))) (literal %5D)) (concept grammar.constructor-attribute) (source-names (tree-sitter _constructor_attr)))
(rule assumption_command normal (seq (choice unordered (token (seq (literal Axiom) (not (ref word_characters)))) (token (seq (literal Axioms) (not (ref word_characters)))) (token (seq (literal Conjecture) (not (ref word_characters)))) (token (seq (literal Conjectures) (not (ref word_characters)))) (token (seq (literal Parameter) (not (ref word_characters)))) (token (seq (literal Parameters) (not (ref word_characters)))) (token (seq (literal Hypothesis) (not (ref word_characters)))) (token (seq (literal Hypotheses) (not (ref word_characters)))) (token (seq (literal Variable) (not (ref word_characters)))) (token (seq (literal Variables) (not (ref word_characters))))) (optional (seq (token (seq (literal Inline) (not (ref word_characters)))) (optional (seq (literal %28) (ref natural) (literal %29))))) (choice unordered (ref assumption) (repeat1 (seq (literal %28) (ref assumption) (literal %29))))) (concept grammar.assumption-command))
(rule assumption normal (seq (repeat1 (ref identifier_declaration)) (ref of_type)) (concept grammar.assumption) (source-names (tree-sitter assumpt)))
(rule of_type normal (seq (choice unordered (literal %3A) (literal %3A%3E)) (ref type)) (concept grammar.of-type))
(rule arguments_command normal (seq (token (seq (literal Arguments) (not (ref word_characters)))) (ref global_reference) (repeat0 (ref argument_specification_item)) (repeat0 (seq (literal %2C) (repeat0 (ref argument_specification_item)))) (optional (seq (literal %3A) (ref arguments_modifier) (repeat0 (seq (literal %2C) (ref arguments_modifier)))))) (concept grammar.arguments-command))
(rule argument_specification_item silent (choice unordered (ref argument_specification) (literal %2F) (literal %26) (seq (literal %28) (repeat1 (ref argument_specification)) (literal %29) (optional (ref scope_key))) (seq (literal %5B) (repeat1 (ref argument_specification)) (literal %5D) (optional (ref scope_key))) (seq (literal %7B) (repeat1 (ref argument_specification)) (literal %7D) (optional (ref scope_key)))) (concept grammar.argument-specification-item) (source-names (tree-sitter _argument_spec_item)))
(rule argument_specification silent (seq (optional (literal %21)) (ref name) (optional (ref scope_key))) (concept grammar.argument-specification) (source-names (tree-sitter _argument_spec)))
(rule scope_key normal (seq (literal %25) (optional (token (seq (literal _) (not (ref word_characters))))) (ref identifier)) (concept grammar.scope-key))
(rule arguments_modifier normal (repeat1 (ref identifier)) (concept grammar.arguments-modifier))
(rule section_command normal (seq (token (seq (literal Section) (not (ref word_characters)))) (ref identifier)) (concept grammar.section-command))
(rule module_command normal (seq (token (seq (literal Module) (not (ref word_characters)))) (optional (choice unordered (token (seq (literal Type) (not (ref word_characters)))) (token (seq (literal Import) (not (ref word_characters)))) (token (seq (literal Export) (not (ref word_characters)))))) (ref identifier) (repeat0 (ref module_binder)) (repeat0 (seq (choice unordered (literal %3A) (literal %3C%3A)) (ref module_type_expression))) (optional (seq (literal %3A%3D) (ref module_type_expression) (repeat0 (seq (literal %3C%2B) (ref module_type_expression)))))) (concept grammar.module-command))
(rule module_binder normal (seq (literal %28) (optional (choice unordered (token (seq (literal Import) (not (ref word_characters)))) (token (seq (literal Export) (not (ref word_characters)))))) (repeat1 (capture labeled name (ref identifier))) (literal %3A) (ref module_type_expression) (literal %29)) (concept grammar.module-binder))
(rule module_type_expression normal (precedence 0 right (seq (ref qualified_identifier) (repeat0 (choice unordered (ref qualified_identifier) (seq (literal %28) (ref module_type_expression) (literal %29)))) (optional (literal %21)) (repeat0 (seq (token (seq (literal with) (not (ref word_characters)))) (choice unordered (seq (token (seq (literal Definition) (not (ref word_characters)))) (ref qualified_identifier) (repeat0 (ref binder)) (literal %3A%3D) (ref term)) (seq (token (seq (literal Module) (not (ref word_characters)))) (ref qualified_identifier) (literal %3A%3D) (ref qualified_identifier))))))) (concept grammar.module-type-expression) (source-names (tree-sitter module_type_expr)))
(rule include_command normal (seq (token (seq (literal Include) (not (ref word_characters)))) (optional (token (seq (literal Type) (not (ref word_characters))))) (ref module_type_expression) (repeat0 (seq (literal %3C%2B) (ref module_type_expression)))) (concept grammar.include-command))
(rule register_command normal (seq (token (seq (literal Register) (not (ref word_characters)))) (optional (choice unordered (token (seq (literal Inline) (not (ref word_characters)))) (token (seq (literal Scheme) (not (ref word_characters)))))) (capture labeled name (ref qualified_identifier)) (optional (seq (token (seq (literal as) (not (ref word_characters)))) (capture labeled key (ref qualified_identifier)))) (optional (seq (token (seq (literal for) (not (ref word_characters)))) (ref qualified_identifier)))) (concept grammar.register-command))
(rule instance_command normal (seq (choice unordered (token (seq (literal Instance) (not (ref word_characters)))) (seq (token (seq (literal Declare) (not (ref word_characters)))) (token (seq (literal Instance) (not (ref word_characters)))))) (optional (seq (capture labeled name (ref identifier_declaration)) (repeat0 (ref binder)))) (literal %3A) (ref type) (optional (ref hint_priority)) (optional (seq (literal %3A%3D) (choice unordered (ref record_fields_literal) (ref term))))) (concept grammar.instance-declaration))
(rule hint_priority normal (seq (literal %7C) (ref natural) (optional (ref one_term))) (concept grammar.hint-priority))
(rule record_fields_literal normal (seq (literal %7B) (optional (seq (ref field_definition) (repeat0 (seq (literal %3B) (ref field_definition))) (optional (literal %3B)))) (literal %7D)) (concept grammar.record-fields-literal))
(rule field_definition normal (seq (capture labeled name (ref qualified_identifier)) (repeat0 (ref binder)) (literal %3A%3D) (capture labeled value (ref term))) (concept grammar.field-definition))
(rule existing_command normal (seq (token (seq (literal Existing) (not (ref word_characters)))) (choice unordered (token (seq (literal Instance) (not (ref word_characters)))) (token (seq (literal Instances) (not (ref word_characters)))) (token (seq (literal Class) (not (ref word_characters))))) (repeat1 (ref qualified_identifier)) (optional (ref hint_priority))) (concept grammar.existing-command))
(rule record_command normal (seq (choice unordered (token (seq (literal Record) (not (ref word_characters)))) (token (seq (literal Structure) (not (ref word_characters)))) (token (seq (literal Class) (not (ref word_characters))))) (capture labeled name (ref identifier_declaration)) (repeat0 (ref binder)) (optional (seq (literal %3A) (ref type))) (optional (seq (literal %3A%3D) (choice unordered (precedence 1 none (seq (optional (capture labeled constructor (ref identifier))) (literal %7B) (optional (seq (ref record_field) (repeat0 (seq (literal %3B) (ref record_field))) (optional (literal %3B)))) (literal %7D))) (ref record_field))))) (concept grammar.record-command))
(rule record_field normal (seq (repeat0 (ref constructor_attribute)) (capture labeled name (ref identifier_declaration)) (repeat0 (ref binder)) (choice unordered (seq (choice unordered (literal %3A) (literal %3A%3E) (literal %3A%3A) (literal %3A%3A%3E)) (ref type) (optional (seq (literal %3A%3D) (ref term)))) (seq (literal %3A%3D) (ref term))) (optional (ref hint_priority)) (optional (ref declaration_notations))) (concept grammar.record-field))
(rule scheme_command normal (seq (token (seq (literal Scheme) (not (ref word_characters)))) (ref scheme_kind) (repeat0 (seq (token (seq (literal with) (not (ref word_characters)))) (ref scheme_kind)))) (concept grammar.scheme-command))
(rule scheme_kind silent (seq (optional (seq (capture labeled name (ref identifier)) (literal %3A%3D))) (optional (token (seq (literal Boolean) (not (ref word_characters))))) (choice unordered (token (seq (literal Induction) (not (ref word_characters)))) (token (seq (literal Minimality) (not (ref word_characters)))) (token (seq (literal Elimination) (not (ref word_characters)))) (token (seq (literal Case) (not (ref word_characters)))) (token (seq (literal Equality) (not (ref word_characters)))) (token (seq (literal Rewriting) (not (ref word_characters))))) (token (seq (literal for) (not (ref word_characters)))) (ref qualified_identifier) (optional (seq (token (seq (literal Sort) (not (ref word_characters)))) (ref identifier)))) (concept grammar.scheme-kind) (source-names (tree-sitter _scheme_kind)))
(rule combined_scheme_command normal (seq (token (seq (literal Combined) (not (ref word_characters)))) (token (seq (literal Scheme) (not (ref word_characters)))) (capture labeled name (ref identifier)) (token (seq (literal from) (not (ref word_characters)))) (ref qualified_identifier) (repeat0 (seq (literal %2C) (ref qualified_identifier)))) (concept grammar.combined-scheme-command))
(rule delimit_scope_command normal (seq (token (seq (literal Delimit) (not (ref word_characters)))) (token (seq (literal Scope) (not (ref word_characters)))) (capture labeled scope (ref identifier)) (token (seq (literal with) (not (ref word_characters)))) (capture labeled key (ref identifier))) (concept grammar.delimit-scope-command))
(rule bind_scope_command normal (seq (token (seq (literal Bind) (not (ref word_characters)))) (token (seq (literal Scope) (not (ref word_characters)))) (capture labeled scope (ref identifier)) (token (seq (literal with) (not (ref word_characters)))) (repeat1 (ref coercion_class))) (concept grammar.bind-scope-command))
(rule context_command normal (seq (token (seq (literal Context) (not (ref word_characters)))) (repeat1 (ref binder))) (concept grammar.context-command))
(rule obligation_tactic_command normal (seq (token (seq (literal Obligation) (not (ref word_characters)))) (token (seq (literal Tactic) (not (ref word_characters)))) (literal %3A%3D) (ref ltac_expression)) (concept grammar.obligation-tactic-command))
(rule obligation_command normal (choice unordered (seq (token (seq (literal Next) (not (ref word_characters)))) (token (seq (literal Obligation) (not (ref word_characters)))) (optional (seq (token (seq (literal of) (not (ref word_characters)))) (ref qualified_identifier)))) (seq (token (seq (literal Obligation) (not (ref word_characters)))) (ref natural) (optional (seq (token (seq (literal of) (not (ref word_characters)))) (ref qualified_identifier))) (optional (seq (literal %3A) (ref type)))) (seq (choice unordered (token (seq (literal Solve) (not (ref word_characters)))) (token (seq (literal Admit) (not (ref word_characters))))) (choice unordered (token (seq (literal Obligations) (not (ref word_characters)))) (seq (token (seq (literal All) (not (ref word_characters)))) (token (seq (literal Obligations) (not (ref word_characters)))))) (optional (seq (token (seq (literal of) (not (ref word_characters)))) (ref qualified_identifier))) (optional (seq (token (seq (literal with) (not (ref word_characters)))) (ref ltac_expression)))) (seq (token (seq (literal Obligations) (not (ref word_characters)))) (optional (seq (token (seq (literal of) (not (ref word_characters)))) (ref qualified_identifier))))) (concept grammar.obligation-command))
(rule implicit_types_command normal (seq (token (seq (literal Implicit) (not (ref word_characters)))) (choice unordered (token (seq (literal Type) (not (ref word_characters)))) (token (seq (literal Types) (not (ref word_characters))))) (choice unordered (seq (repeat1 (ref identifier)) (literal %3A) (ref type)) (repeat1 (seq (literal %28) (repeat1 (ref identifier)) (literal %3A) (ref type) (literal %29))))) (concept grammar.implicit-types-command))
(rule type_classes_command normal (seq (token (seq (literal Typeclasses) (not (ref word_characters)))) (choice unordered (token (seq (literal Opaque) (not (ref word_characters)))) (token (seq (literal Transparent) (not (ref word_characters))))) (repeat1 (ref qualified_identifier))) (concept grammar.type-classes-command) (source-names (tree-sitter typeclasses_command)))
(rule generalizable_command normal (seq (token (seq (literal Generalizable) (not (ref word_characters)))) (choice unordered (seq (token (seq (literal All) (not (ref word_characters)))) (token (seq (literal Variables) (not (ref word_characters))))) (seq (token (seq (literal No) (not (ref word_characters)))) (token (seq (literal Variables) (not (ref word_characters))))) (seq (choice unordered (token (seq (literal Variable) (not (ref word_characters)))) (token (seq (literal Variables) (not (ref word_characters))))) (repeat1 (ref identifier))))) (concept grammar.generalizable-command))
(rule end_command normal (seq (token (seq (literal End) (not (ref word_characters)))) (ref identifier)) (concept grammar.end-command))
(rule reserved_notation_command normal (seq (token (seq (literal Reserved) (not (ref word_characters)))) (token (seq (literal Notation) (not (ref word_characters)))) (capture labeled notation (ref string)) (optional (ref syntax_modifier_list))) (concept grammar.reserved-notation-command))
(rule notation_command normal (seq (token (seq (literal Notation) (not (ref word_characters)))) (ref notation_declaration)) (concept grammar.notation-command))
(rule infix_command normal (seq (token (seq (literal Infix) (not (ref word_characters)))) (ref notation_declaration)) (concept grammar.infix-command))
(rule abbreviation_command normal (seq (choice unordered (token (seq (literal Abbreviation) (not (ref word_characters)))) (token (seq (literal Notation) (not (ref word_characters))))) (capture labeled name (ref identifier)) (repeat0 (ref identifier)) (literal %3A%3D) (capture labeled definition (ref one_term)) (optional (ref syntax_modifier_list))) (concept grammar.abbreviation-command))
(rule notation_declaration normal (seq (capture labeled notation (ref string)) (literal %3A%3D) (capture labeled definition (ref one_term)) (optional (ref syntax_modifier_list)) (optional (ref notation_scope))) (concept grammar.notation-declaration))
(rule notation_scope normal (seq (literal %3A) (capture labeled scope_name (ref identifier))) (concept grammar.notation-scope))
(rule syntax_modifier_list normal (seq (literal %28) (ref syntax_modifier) (repeat0 (seq (literal %2C) (ref syntax_modifier))) (optional (literal %2C)) (literal %29)) (concept grammar.syntax-modifier-list))
(rule syntax_modifier normal (choice unordered (ref level_modifier) (ref custom_entry_modifier) (ref associativity_modifier) (ref parsing_modifier) (ref printing_modifier) (ref format_modifier) (ref plural_variable_modifier) (ref singular_variable_modifier)) (concept grammar.syntax-modifier))
(rule level_modifier normal (ref at_level_number) (concept grammar.level-modifier))
(rule custom_entry_modifier normal (seq (token (seq (literal in) (not (ref word_characters)))) (token (seq (literal custom) (not (ref word_characters)))) (ref qualified_identifier) (optional (ref at_level_number))) (concept grammar.custom-entry-modifier))
(rule associativity_modifier normal (seq (choice unordered (token (seq (literal left) (not (ref word_characters)))) (token (seq (literal right) (not (ref word_characters)))) (token (seq (literal no) (not (ref word_characters))))) (token (seq (literal associativity) (not (ref word_characters))))) (concept grammar.associativity-modifier))
(rule parsing_modifier normal (seq (token (seq (literal only) (not (ref word_characters)))) (token (seq (literal parsing) (not (ref word_characters))))) (concept grammar.parsing-modifier))
(rule printing_modifier normal (seq (token (seq (literal only) (not (ref word_characters)))) (token (seq (literal printing) (not (ref word_characters))))) (concept grammar.printing-modifier))
(rule format_modifier normal (seq (token (seq (literal format) (not (ref word_characters)))) (ref string)) (concept grammar.format-modifier))
(rule plural_variable_modifier normal (seq (ref identifier) (repeat1 (seq (literal %2C) (ref identifier))) (choice unordered (ref at_level) (seq (token (seq (literal in) (not (ref word_characters)))) (token (seq (literal scope) (not (ref word_characters)))) (ref identifier)))) (concept grammar.plural-variable-modifier))
(rule singular_variable_modifier normal (seq (ref identifier) (choice unordered (seq (token (seq (literal in) (not (ref word_characters)))) (token (seq (literal scope) (not (ref word_characters)))) (ref identifier)) (seq (token (seq (literal at) (not (ref word_characters)))) (ref level) (optional (ref binder_interpretation))) (ref explicit_notation_entry) (ref binder_interpretation))) (concept grammar.singular-variable-modifier))
(rule explicit_notation_entry normal (choice unordered (token (seq (literal ident) (not (ref word_characters)))) (token (seq (literal name) (not (ref word_characters)))) (token (seq (literal global) (not (ref word_characters)))) (token (seq (literal bigint) (not (ref word_characters)))) (seq (token (seq (literal strict) (not (ref word_characters)))) (token (seq (literal pattern) (not (ref word_characters)))) (optional (ref at_level_number))) (token (seq (literal binder) (not (ref word_characters)))) (seq (token (seq (literal closed) (not (ref word_characters)))) (token (seq (literal binder) (not (ref word_characters))))) (seq (token (seq (literal constr) (not (ref word_characters)))) (optional (ref at_level)) (optional (ref binder_interpretation))) (seq (token (seq (literal custom) (not (ref word_characters)))) (ref identifier) (optional (ref at_level)) (optional (ref binder_interpretation))) (seq (token (seq (literal pattern) (not (ref word_characters)))) (optional (ref at_level_number)))) (concept grammar.explicit-notation-entry) (source-names (tree-sitter explicit_subentry)))
(rule binder_interpretation normal (seq (token (seq (literal as) (not (ref word_characters)))) (choice unordered (token (seq (literal ident) (not (ref word_characters)))) (token (seq (literal name) (not (ref word_characters)))) (token (seq (literal pattern) (not (ref word_characters)))) (seq (token (seq (literal strict) (not (ref word_characters)))) (token (seq (literal pattern) (not (ref word_characters))))))) (concept grammar.binder-interpretation) (source-names (tree-sitter binder_interp)))
(rule level normal (choice unordered (seq (token (seq (literal level) (not (ref word_characters)))) (ref natural)) (seq (token (seq (literal next) (not (ref word_characters)))) (token (seq (literal level) (not (ref word_characters)))))) (concept grammar.level))
(rule at_level_number normal (seq (token (seq (literal at) (not (ref word_characters)))) (token (seq (literal level) (not (ref word_characters)))) (ref natural)) (concept grammar.at-level-number) (source-names (tree-sitter at_level_num)))
(rule at_level normal (seq (token (seq (literal at) (not (ref word_characters)))) (ref level)) (concept grammar.at-level))
(rule proof_command normal (seq (token (seq (literal Proof) (not (ref word_characters)))) (optional (choice unordered (seq (token (seq (literal using) (not (ref word_characters)))) (ref section_variable_expression) (optional (seq (token (seq (literal with) (not (ref word_characters)))) (ref ltac_expression)))) (seq (token (seq (literal with) (not (ref word_characters)))) (ref ltac_expression) (optional (seq (token (seq (literal using) (not (ref word_characters)))) (ref section_variable_expression))))))) (concept grammar.proof-command))
(rule section_variable_expression normal (choice unordered (seq (ref expression_leaf) (repeat1 (ref expression_leaf))) (seq (optional (literal -)) (ref expression_ops))) (concept grammar.section-variable-expression) (source-names (tree-sitter section_var_expr)))
(rule expression_ops normal (choice unordered (seq (ref atomic_expression) (literal -) (ref atomic_expression)) (seq (ref atomic_expression) (literal %2B) (ref atomic_expression)) (ref atomic_expression)) (concept grammar.expression-ops) (source-names (tree-sitter expr_ops)))
(rule atomic_expression normal (choice unordered (ref expression_leaf) (seq (literal %28) (literal %29)) (seq (literal %28) (ref section_variable_expression) (literal %29) (optional (literal %2A)))) (concept grammar.atomic-expression) (source-names (tree-sitter expr_atomic)))
(rule expression_leaf normal (choice unordered (seq (ref identifier) (optional (literal %2A))) (seq (token (seq (literal Type) (not (ref word_characters)))) (optional (literal %2A))) (token (seq (literal All) (not (ref word_characters))))) (concept grammar.expression-leaf) (source-names (tree-sitter expr_leaf)))
(rule qed_command token (seq (literal Qed) (not (ref word_characters))) (concept grammar.qed-command))
(rule admitted_command token (seq (literal Admitted) (not (ref word_characters))) (concept grammar.admitted-command))
(rule save_command normal (seq (token (seq (literal Save) (not (ref word_characters)))) (ref identifier)) (concept grammar.save-command))
(rule defined_command normal (seq (token (seq (literal Defined) (not (ref word_characters)))) (optional (ref identifier))) (concept grammar.defined-command))
(rule abort_command normal (seq (token (seq (literal Abort) (not (ref word_characters)))) (optional (token (seq (literal All) (not (ref word_characters)))))) (concept grammar.abort-command))
(rule proof_block normal (seq (optional (ref selector)) (literal %7B) (repeat0 (ref sentence)) (literal %7D)) (concept grammar.proof-block))
(rule bullet token (repeat1 (class plain (char %2B) (char %2A) (char -))) (concept grammar.bullet))
(rule term silent (ref hundred_level_term) (concept grammar.term) (source-names (tree-sitter _term)))
(rule hundred_level_term silent (choice unordered (ref term_cast) (ref ninety_nine_level_term)) (concept grammar.hundred-level-term) (source-names (tree-sitter _term100)))
(rule term_cast normal (namedPrecedence type right (seq (ref ninety_nine_level_term) (choice unordered (literal %3A) (literal %3C%3A) (literal %3C%3C%3A) (literal %3A%3E)) (ref type))) (concept grammar.term-cast))
(rule ninety_nine_level_term silent (ref ten_level_term) (concept grammar.ninety-nine-level-term) (source-names (tree-sitter _term99)))
(rule ten_level_term silent (choice unordered (ref application) (ref lambda_function) (ref quantifier_term) (ref let_expression) (ref fix_expression) (ref if_expression) (ref one_term) (ref arrow_term) (ref infix_operation) (ref imp_evaluation_operation) (ref rewrite_term)) (concept grammar.ten-level-term) (source-names (tree-sitter _term10)))
(rule rewrite_term normal (namedPrecedence binder right (seq (token (seq (literal rew) (not (ref word_characters)))) (optional (choice unordered (literal %3C-) (literal -%3E))) (optional (token (seq (literal dependent) (not (ref word_characters))))) (optional (seq (literal %5B) (ref term) (literal %5D))) (ref term) (token (seq (literal in) (not (ref word_characters)))) (ref term))) (concept grammar.rewrite-term) (source-names (tree-sitter rew_term)))
(rule one_term silent (choice unordered (seq (literal %40) (ref qualified_identifier)) (ref one_level_term)) (concept grammar.one-term) (source-names (tree-sitter _one_term)))
(rule one_level_term silent (choice unordered (ref scoped_term) (ref zero_level_term)) (concept grammar.one-level-term) (source-names (tree-sitter _term1)))
(rule zero_level_term silent (seq (optional (literal %27)) (choice unordered (ref annotated_qualified_identifier) (ref number) (ref string) (ref match_expression) (ref parenthesized_term) (ref metavariable) (ref list_literal) (ref subset_term) (ref projection_term) (ref recursive_notation_term) (ref custom_notation_block) (ref ltac_quotation) (ref term_quotation))) (concept grammar.zero-level-term) (source-names (tree-sitter _term0)))
(rule ltac_quotation normal (seq (literal ltac%3A%28) (ref ltac_expression) (literal %29)) (concept grammar.ltac-quotation))
(rule term_quotation normal (seq (choice unordered (literal constr%3A%28) (literal open_constr%3A%28) (literal uconstr%3A%28) (literal type_term%3A%28)) (ref term) (literal %29)) (concept grammar.term-quotation))
(rule subset_term normal (choice unordered (dynamicPrecedence 1 (seq (literal %7B) (choice unordered (ref name) (ref destructuring_pattern)) (optional (seq (literal %3A) (ref type))) (choice unordered (literal %7C) (literal %26)) (ref term) (optional (seq (literal %26) (ref term))) (literal %7D))) (seq (literal %7B) (ref term) (literal %7D))) (concept grammar.subset-term))
(rule projection_term normal (namedPrecedence scope left (seq (choice unordered (ref qualified_identifier) (ref parenthesized_term) (ref projection_term)) (choice unordered (alias unnamed_token (immediateToken (seq (literal .) (repeat1 (class plain (range 0 9)))))) (seq (immediateToken (literal .%28)) (optional (literal %40)) (ref qualified_identifier) (repeat0 (ref argument)) (literal %29))))) (concept grammar.projection-term))
(rule double_dot token (literal ..) (concept grammar.double-dot))
(rule recursive_notation_term normal (seq (ref double_dot) (ref zero_level_term) (ref double_dot)) (concept grammar.recursive-notation-term))
(rule parenthesized_term normal (seq (literal %28) (optional (literal %3D)) (ref term) (optional (choice unordered (repeat1 (seq (literal %2C) (ref term))) (repeat1 (seq (literal %3B) (ref term))))) (optional (choice unordered (literal %2C) (literal %3B))) (literal %29)) (concept grammar.parenthesized-term))
(rule list_literal normal (seq (literal %5B) (optional (seq (ref term) (repeat0 (seq (literal %3B) (ref term))) (optional (literal %3B)))) (literal %5D)) (concept grammar.list-literal))
(rule scoped_term normal (namedPrecedence scope left (seq (ref one_level_term) (literal %25) (optional (token (seq (literal _) (not (ref word_characters))))) (ref identifier))) (concept grammar.scoped-term))
(rule application normal (namedPrecedence application left (seq (ref term) (repeat1 (ref argument)))) (concept grammar.function-application))
(rule argument silent (choice unordered (seq (literal %28) (ref identifier) (literal %3A%3D) (ref term) (literal %29)) (seq (literal %28) (ref natural) (literal %3A%3D) (ref term) (literal %29)) (ref one_level_term)) (concept argument) (source-names (tree-sitter _arg)))
(rule lambda_function normal (namedPrecedence binder none (seq (token (seq (literal fun) (not (ref word_characters)))) (ref open_binders) (literal %3D%3E) (ref term))) (concept grammar.lambda-function))
(rule quantifier_term normal (namedPrecedence quantifier_term right (seq (choice unordered (token (seq (literal forall) (not (ref word_characters)))) (token (seq (literal exists) (not (ref word_characters)))) (literal exists%21) (token (seq (literal exists2) (not (ref word_characters)))) (literal %E2%88%80) (literal %E2%88%83) (literal %E2%88%83%21)) (ref open_binders) (literal %2C) (ref type))) (concept grammar.quantifier-term))
(rule let_expression normal (choice unordered (ref let_expression_term) (ref destructuring_let_name_list) (ref destructuring_let_apostrophe)) (concept grammar.let-expression))
(rule let_expression_term silent (namedPrecedence binder right (seq (token (seq (literal let) (not (ref word_characters)))) (capture labeled name (ref name)) (repeat0 (ref binder)) (optional (seq (literal %3A) (ref type))) (literal %3A%3D) (capture labeled value (ref term)) (token (seq (literal in) (not (ref word_characters)))) (capture labeled body (ref term)))) (concept grammar.let-expression-term) (source-names (tree-sitter _let_expression_term)))
(rule destructuring_let_name_list silent (namedPrecedence binder right (seq (token (seq (literal let) (not (ref word_characters)))) (capture labeled pattern (ref let_expression_name_list)) (optional (ref term_as_clause)) (optional (ref term_return_clause)) (literal %3A%3D) (capture labeled value (ref term)) (token (seq (literal in) (not (ref word_characters)))) (capture labeled body (ref term)))) (concept grammar.destructuring-let-name-list) (source-names (tree-sitter _destructuring_let_name_list)))
(rule destructuring_let_apostrophe silent (namedPrecedence binder right (seq (token (seq (literal let) (not (ref word_characters)))) (capture labeled pattern (ref destructuring_pattern)) (optional (ref term_in_pattern)) (literal %3A%3D) (capture labeled value (ref term)) (optional (ref term_return_clause)) (token (seq (literal in) (not (ref word_characters)))) (capture labeled body (ref term)))) (concept grammar.destructuring-let-apostrophe) (source-names (tree-sitter _destructuring_let_apos)))
(rule let_expression_name_list normal (seq (literal %28) (optional (seq (ref name) (repeat0 (seq (literal %2C) (ref name))))) (literal %29)) (concept grammar.let-expression-name-list))
(rule match_expression normal (seq (token (seq (literal match) (not (ref word_characters)))) (ref match_item) (repeat0 (seq (literal %2C) (ref match_item))) (optional (ref term_return_clause)) (token (seq (literal with) (not (ref word_characters)))) (optional (choice unordered (seq (ref match_case) (repeat0 (seq (literal %7C) (ref match_case)))) (repeat1 (seq (literal %7C) (ref match_case))))) (token (seq (literal end) (not (ref word_characters))))) (concept grammar.match-expression))
(rule match_item normal (seq (ref hundred_level_term) (optional (ref term_as_clause)) (optional (ref term_in_pattern))) (concept grammar.match-item) (source-names (tree-sitter case_item)))
(rule match_case normal (seq (ref pattern_option) (repeat0 (seq (literal %7C) (ref pattern_option))) (literal %3D%3E) (capture labeled body (ref term))) (concept grammar.match-case))
(rule pattern_option normal (seq (capture labeled pattern (ref pattern)) (repeat0 (seq (literal %2C) (capture labeled pattern (ref pattern))))) (concept grammar.pattern-option))
(rule if_expression normal (namedPrecedence binder right (seq (token (seq (literal if) (not (ref word_characters)))) (capture labeled condition (ref term)) (optional (ref term_as_clause)) (optional (ref term_return_clause)) (token (seq (literal then) (not (ref word_characters)))) (capture labeled then (ref term)) (token (seq (literal else) (not (ref word_characters)))) (capture labeled else (ref term)))) (concept grammar.if-expression))
(rule fix_expression normal (precedence 0 right (seq (token (seq (literal fix) (not (ref word_characters)))) (ref fix_declaration) (optional (seq (repeat1 (seq (token (seq (literal with) (not (ref word_characters)))) (ref fix_declaration))) (token (seq (literal for) (not (ref word_characters)))) (ref identifier))))) (concept grammar.fix-expression))
(rule fix_declaration normal (precedence 0 right (seq (capture labeled name (ref identifier)) (repeat0 (ref binder)) (optional (ref fixpoint_annotation)) (optional (seq (literal %3A) (ref type))) (literal %3A%3D) (capture labeled body (ref term)))) (concept grammar.fix-declaration) (source-names (tree-sitter fix_decl)))
(rule term_as_clause normal (seq (token (seq (literal as) (not (ref word_characters)))) (capture labeled as_name (ref name))) (concept grammar.term-as-clause))
(rule term_return_clause normal (seq (token (seq (literal return) (not (ref word_characters)))) (capture labeled as_return (ref hundred_level_term))) (concept grammar.term-return-clause))
(rule term_in_pattern normal (precedence 0 left (seq (token (seq (literal in) (not (ref word_characters)))) (capture labeled in_pattern (ref pattern)))) (concept grammar.term-in-pattern))
(rule infix_operation silent (choice unordered (ref negation_operation) (ref cons_operation) (ref append_operation) (ref multiplicative_operation) (ref additive_operation) (ref comparison_operation) (ref logical_conjunction) (ref logical_disjunction) (ref logical_equivalence) (ref custom_operation)) (concept grammar.infix-operation) (source-names (tree-sitter _infix_operation)))
(rule negation_operation normal (namedPrecedence negation left (seq (literal %7E) (ref term))) (concept grammar.negation-operation))
(rule cons_operation normal (namedPrecedence list_ops right (seq (ref term) (literal %3A%3A) (ref term))) (concept grammar.cons-operation))
(rule append_operation normal (namedPrecedence list_ops right (seq (ref term) (literal %2B%2B) (ref term))) (concept grammar.append-operation) (source-names (tree-sitter app_operation)))
(rule multiplicative_operation normal (namedPrecedence multiplicative left (seq (ref term) (choice unordered (literal %2A) (literal %2F)) (ref term))) (concept grammar.multiplicative-operation))
(rule additive_operation normal (namedPrecedence additive left (seq (ref term) (choice unordered (literal %2B) (literal -)) (ref term))) (concept grammar.additive-operation))
(rule comparison_operation normal (namedPrecedence comparison left (seq (ref term) (choice unordered (literal %3D) (literal %3C%3E) (literal %3C) (literal %3C%3D) (literal %3E) (literal %3E%3D) (literal %3D%3F) (literal %3C%3E%3F) (literal %3C%3F) (literal %3C%3D%3F) (literal %3E%3F) (literal %3E%3D%3F)) (ref term))) (concept grammar.comparison-operation))
(rule logical_conjunction normal (namedPrecedence conjunction right (seq (ref term) (literal %2F%5C) (ref term))) (concept grammar.logical-conjunction))
(rule logical_disjunction normal (namedPrecedence disjunction right (seq (ref term) (literal %5C%2F) (ref term))) (concept grammar.logical-disjunction))
(rule logical_equivalence normal (namedPrecedence equivalence left (seq (ref term) (literal %3C-%3E) (ref term))) (concept grammar.logical-equivalence))
(rule custom_operation normal (namedPrecedence custom left (seq (ref term) (alias custom_operator (choice unordered (alias unnamed_token (token (repeat1 (class plain (char -) (char %21) (char %23) (char %24) (char %25) (char %26) (char %2A) (char %2B) (char %2F) (char %3C) (char %3D) (char %3E) (char %3F) (char %40) (char %5E) (char %7C) (char %7E) (char %3B))))) (alias unnamed_token (token (seq (repeat0 (class plain (char -) (char %21) (char %23) (char %24) (char %25) (char %26) (char %2A) (char %2B) (char .) (char %2F) (char %3C) (char %3D) (char %3E) (char %3F) (char %40) (char %5E) (char %7C) (char %7E) (char %3B))) (class plain (char -) (char %21) (char %23) (char %24) (char %25) (char %26) (char %2A) (char %2B) (char %2F) (char %3C) (char %3D) (char %3E) (char %3F) (char %40) (char %5E) (char %7C) (char %7E) (char %3B)) (repeat0 (class plain (char -) (char %21) (char %23) (char %24) (char %25) (char %26) (char %2A) (char %2B) (char .) (char %2F) (char %3C) (char %3D) (char %3E) (char %3F) (char %40) (char %5E) (char %7C) (char %7E) (char %3B)))))) (alias unnamed_token (token (seq (literal .) (literal .)))) (alias unnamed_token (token (seq (literal ...) (repeat1 (literal .))))))) (ref term))) (concept grammar.custom-operation))
(rule arrow_term normal (namedPrecedence arrow_term right (seq (capture labeled antecedent (ref term)) (literal -%3E) (capture labeled consequent (ref term)))) (concept grammar.arrow-term))
(rule pattern silent (precedence 0 right (choice unordered (ref ten_level_pattern) (seq (ref ten_level_pattern) (literal %3A) (ref term)) (ref infix_pattern) (ref custom_notation_block))) (concept grammar.pattern) (source-names (tree-sitter _pattern)))
(rule infix_pattern normal (namedPrecedence list_ops right (seq (ref pattern) (choice unordered (literal %3A%3A) (literal %2B%2B) (literal %3D) (literal %3C%3E) (literal %2B) (literal %2A) (literal %2F%5C) (literal %5C%2F) (literal %26)) (ref pattern))) (concept grammar.infix-pattern))
(rule ten_level_pattern silent (precedence 0 right (choice unordered (seq (ref ten_level_pattern) (token (seq (literal as) (not (ref word_characters)))) (ref name)) (ref pattern_application) (seq (literal %40) (ref qualified_identifier) (repeat0 (ref one_level_pattern))) (ref one_level_pattern))) (concept grammar.ten-level-pattern) (source-names (tree-sitter _pattern10)))
(rule pattern_application normal (namedPrecedence application left (seq (ref ten_level_pattern) (repeat1 (ref one_level_pattern)))) (concept grammar.pattern-application))
(rule one_level_pattern silent (choice unordered (seq (ref one_level_pattern) (literal %25) (optional (token (seq (literal _) (not (ref word_characters))))) (ref identifier)) (ref zero_level_pattern)) (concept grammar.one-level-pattern) (source-names (tree-sitter _pattern1)))
(rule zero_level_pattern silent (choice unordered (ref qualified_identifier) (ref wildcard) (seq (literal %7B) (literal %7C) (repeat0 (seq (ref qualified_identifier) (literal %3A%3D) (ref pattern))) (literal %7C) (literal %7D)) (ref parenthesized_pattern) (ref number) (ref string) (ref list_pattern)) (concept grammar.zero-level-pattern) (source-names (tree-sitter _pattern0)))
(rule parenthesized_pattern normal (seq (literal %28) (ref pattern) (repeat0 (seq (choice unordered (literal %7C) (literal %2C)) (ref pattern))) (literal %29)) (concept grammar.parenthesized-pattern))
(rule list_pattern normal (seq (literal %5B) (optional (seq (ref pattern) (repeat0 (seq (literal %3B) (ref pattern))))) (literal %5D)) (concept grammar.list-pattern))
(rule destructuring_pattern normal (precedence 0 right (seq (literal %27) (ref pattern))) (concept grammar.destructuring-pattern))
(rule type normal (precedence 0 right (ref term)) (concept grammar.type))
(rule name silent (choice unordered (ref wildcard) (ref qualified_identifier)) (concept grammar.name) (source-names (tree-sitter _name)))
(rule binder normal (choice unordered (ref name) (seq (literal %28) (repeat0 (ref name)) (literal %3A) (ref type) (literal %29)) (seq (literal %28) (ref name) (optional (seq (literal %3A) (ref type))) (literal %3A%3D) (ref term) (literal %29)) (ref implicit_binders) (seq (literal %28) (ref name) (literal %3A) (ref type) (literal %7C) (ref term) (literal %29)) (ref destructuring_pattern) (ref generalized_binder)) (concept grammar.single-binder))
(rule generalized_binder normal (seq (literal %60) (choice unordered (seq (literal %28) (ref term) (repeat0 (seq (literal %2C) (ref term))) (literal %29)) (seq (literal %7B) (ref term) (repeat0 (seq (literal %2C) (ref term))) (literal %7D)) (seq (literal %5B) (ref term) (repeat0 (seq (literal %2C) (ref term))) (literal %5D)))) (concept grammar.generalized-binder))
(rule implicit_binders normal (choice unordered (seq (literal %7B) (repeat1 (ref name)) (optional (seq (literal %3A) (ref type))) (literal %7D)) (seq (literal %5B) (repeat1 (ref name)) (optional (seq (literal %3A) (ref type))) (literal %5D))) (concept grammar.implicit-binder))
(rule open_binders normal (seq (repeat1 (ref binder)) (optional (seq (literal %3A) (ref type)))) (concept grammar.open-binders))
(rule ltac_definition normal (seq (token (seq (literal Ltac) (not (ref word_characters)))) (ref ltac_definition_body) (repeat0 (seq (token (seq (literal with) (not (ref word_characters)))) (ref ltac_definition_body)))) (concept grammar.ltac-definition))
(rule ltac_definition_body silent (seq (capture labeled name (ref qualified_identifier)) (repeat0 (ref identifier)) (choice unordered (literal %3A%3D) (literal %3A%3A%3D)) (capture labeled body (ref ltac_expression))) (concept grammar.ltac-definition-body) (source-names (tree-sitter _ltac_definition_body)))
(rule ltac_expression silent (choice unordered (ref parenthesized_tactic) (ref tactic_sequence) (ref tactic_branch) (ref tactic_invocation) (ref tactic_alternative) (ref match_goal) (ref match_ltac_term) (ref ltac_let) (ref ltac_fun) (ref ltac_evaluation) (ref try_if_tactic) (ref term_quotation)) (concept grammar.ltac-expression) (source-names (tree-sitter _ltac_expr)))
(rule ltac_fun normal (namedPrecedence tactic_let right (seq (token (seq (literal fun) (not (ref word_characters)))) (repeat1 (ref identifier)) (literal %3D%3E) (capture labeled body (ref ltac_expression)))) (concept grammar.ltac-fun))
(rule ltac_evaluation normal (namedPrecedence tactic_application right (seq (token (seq (literal eval) (not (ref word_characters)))) (ref reduction_expression) (token (seq (literal in) (not (ref word_characters)))) (ref term))) (concept grammar.ltac-evaluation) (source-names (tree-sitter ltac_eval)))
(rule try_if_tactic normal (namedPrecedence tactic_let right (seq (token (seq (literal tryif) (not (ref word_characters)))) (capture labeled condition (ref ltac_expression)) (token (seq (literal then) (not (ref word_characters)))) (capture labeled consequence (ref ltac_expression)) (token (seq (literal else) (not (ref word_characters)))) (capture labeled alternative (ref ltac_expression)))) (concept grammar.try-if-tactic) (source-names (tree-sitter tryif_tactic)))
(rule match_ltac_term normal (seq (choice unordered (token (seq (literal match) (not (ref word_characters)))) (token (seq (literal lazymatch) (not (ref word_characters)))) (token (seq (literal multimatch) (not (ref word_characters))))) (capture labeled scrutinee (ref term)) (token (seq (literal with) (not (ref word_characters)))) (optional (literal %7C)) (ref match_ltac_case) (repeat0 (seq (literal %7C) (ref match_ltac_case))) (token (seq (literal end) (not (ref word_characters))))) (concept grammar.match-ltac-term))
(rule match_ltac_case normal (seq (ref match_pattern) (literal %3D%3E) (ref ltac_expression)) (concept grammar.match-ltac-case))
(rule ltac_let normal (namedPrecedence tactic_let right (seq (token (seq (literal let) (not (ref word_characters)))) (optional (token (seq (literal rec) (not (ref word_characters))))) (capture labeled name (ref identifier)) (repeat0 (ref identifier)) (literal %3A%3D) (capture labeled value (ref ltac_expression)) (token (seq (literal in) (not (ref word_characters)))) (capture labeled body (ref ltac_expression)))) (concept grammar.ltac-let))
(rule parenthesized_tactic normal (seq (literal %28) (ref ltac_expression) (literal %29)) (concept grammar.parenthesized-tactic))
(rule tactic_sequence normal (namedPrecedence tactic_sequence left (seq (ref ltac_expression) (literal %3B) (ref ltac_expression))) (concept grammar.tactic-sequence))
(rule tactic_branch normal (seq (ref ltac_expression) (literal %3B) (literal %5B) (optional (ref for_each_goal)) (literal %5D)) (concept grammar.tactic-branch))
(rule for_each_goal silent (ref goal_tactics) (concept grammar.for-each-goal) (source-names (tree-sitter _for_each_goal)))
(rule goal_tactics silent (namedPrecedence tactic_sequence left (choice unordered (ref goal_branch) (seq (optional (ref goal_branch)) (repeat1 (seq (literal %7C) (optional (ref goal_branch))))))) (concept grammar.goal-tactics) (source-names (tree-sitter _goal_tactics)))
(rule goal_branch normal (choice unordered (seq (ref ltac_expression) (optional (ref double_dot))) (ref double_dot)) (concept grammar.goal-branch))
(rule tactic_invocation normal (choice unordered (ref first_tactic) (ref intros_tactic) (ref assert_tactic) (ref rewrite_tactic) (ref tactical) (ref generic_tactic)) (concept grammar.tactic-invocation))
(rule intros_tactic normal (seq (choice unordered (token (seq (literal intro) (not (ref word_characters)))) (token (seq (literal intros) (not (ref word_characters))))) (repeat0 (ref intro_pattern))) (concept grammar.intros-tactic))
(rule assert_tactic normal (precedence 0 right (seq (token (seq (literal assert) (not (ref word_characters)))) (choice unordered (seq (literal %28) (ref identifier) (literal %3A) (ref type) (literal %29) (optional (ref by_clause))) (seq (literal %28) (ref identifier) (literal %3A%3D) (ref term) (literal %29)) (seq (ref one_type) (optional (ref as_clause)) (optional (ref by_clause)))))) (concept grammar.assert-tactic))
(rule one_type silent (ref one_term) (concept grammar.one-type) (source-names (tree-sitter _one_type)))
(rule rewrite_tactic normal (namedPrecedence tactic_application left (seq (token (seq (literal rewrite) (not (ref word_characters)))) (ref oriented_rewriter) (repeat0 (seq (literal %2C) (ref oriented_rewriter))) (optional (ref in_clause)) (optional (ref by_clause)))) (concept grammar.rewrite-tactic))
(rule oriented_rewriter normal (precedence 0 right (seq (optional (choice unordered (literal %3C-) (literal -%3E))) (optional (alias decimal_natural_number (token (lexicalPrecedence 1 (repeat1 (class plain (range 0 9))))))) (optional (choice unordered (literal %3F) (literal %21))) (ref atomic_term_with_bindings) (optional (ref at_clause)))) (concept grammar.oriented-rewriter))
(rule at_clause normal (precedence 0 right (seq (token (seq (literal at) (not (ref word_characters)))) (optional (literal -)) (repeat1 (ref natural)))) (concept grammar.at-clause))
(rule atomic_term_with_bindings normal (precedence 0 right (seq (ref one_term) (optional (seq (token (seq (literal with) (not (ref word_characters)))) (ref tactic_bindings))))) (concept grammar.atomic-term-with-bindings))
(rule first_tactic normal (seq (choice unordered (token (seq (literal first) (not (ref word_characters)))) (token (seq (literal solve) (not (ref word_characters))))) (literal %5B) (optional (ref goal_tactics)) (literal %5D)) (concept grammar.first-tactic))
(rule tactical normal (namedPrecedence tactic_application none (seq (choice unordered (token (seq (literal repeat) (not (ref word_characters)))) (token (seq (literal try) (not (ref word_characters)))) (token (seq (literal once) (not (ref word_characters)))) (token (seq (literal progress) (not (ref word_characters)))) (token (seq (literal abstract) (not (ref word_characters)))) (token (seq (literal now) (not (ref word_characters)))) (token (seq (literal exactly_once) (not (ref word_characters)))) (token (seq (literal time) (not (ref word_characters)))) (seq (token (seq (literal do) (not (ref word_characters)))) (choice unordered (ref natural) (ref identifier))) (seq (token (seq (literal timeout) (not (ref word_characters)))) (choice unordered (ref natural) (ref identifier)))) (ref ltac_expression))) (concept grammar.tactical))
(rule generic_tactic normal (dynamicPrecedence 0 (seq (capture labeled name (ref qualified_identifier)) (optional (ref generic_tactic_body)) (repeat0 (seq (literal %2C) (ref generic_tactic_body))) (optional (literal %2C)))) (concept grammar.generic-tactic))
(rule generic_tactic_body normal (choice unordered (seq (repeat1 (ref tactic_argument)) (repeat0 (ref tactic_clause))) (repeat1 (ref tactic_clause))) (concept grammar.generic-tactic-body))
(rule tactic_clause silent (choice unordered (ref in_clause) (ref at_clause) (ref with_clause) (ref as_clause) (ref equation_clause) (ref by_clause) (ref using_clause)) (concept grammar.tactic-clause) (source-names (tree-sitter _tactic_clause)))
(rule tactic_argument silent (choice unordered (ref atomic_term_with_bindings) (ref local_definition) (ref oriented_term)) (concept grammar.tactic-argument) (source-names (tree-sitter _tactic_arg)))
(rule oriented_term normal (seq (choice unordered (literal -%3E) (literal %3C-)) (ref atomic_term_with_bindings)) (concept grammar.oriented-term))
(rule local_definition normal (seq (literal %28) (capture labeled name (ref identifier)) (optional (seq (literal %3A) (ref type))) (literal %3A%3D) (capture labeled value (ref term)) (literal %29)) (concept grammar.local-definition))
(rule tactic_alternative normal (namedPrecedence tactic_or left (seq (ref ltac_expression) (choice unordered (literal %2B) (literal %7C%7C)) (ref ltac_expression))) (concept grammar.tactic-alternative) (source-names (tree-sitter tactic_or)))
(rule match_goal normal (seq (choice unordered (token (seq (literal match) (not (ref word_characters)))) (token (seq (literal lazymatch) (not (ref word_characters)))) (token (seq (literal multimatch) (not (ref word_characters))))) (optional (token (seq (literal reverse) (not (ref word_characters))))) (token (seq (literal goal) (not (ref word_characters)))) (token (seq (literal with) (not (ref word_characters)))) (choice unordered (repeat1 (seq (literal %7C) (ref match_goal_case))) (seq (ref match_goal_case) (repeat0 (seq (literal %7C) (ref match_goal_case)))) (optional (literal %7C))) (token (seq (literal end) (not (ref word_characters))))) (concept grammar.match-goal))
(rule match_goal_case normal (seq (ref goal_pattern) (literal %3D%3E) (ref ltac_expression)) (concept grammar.match-goal-case))
(rule goal_pattern normal (choice unordered (ref goal_pattern_body) (seq (literal %5B) (ref goal_pattern_body) (literal %5D)) (token (seq (literal _) (not (ref word_characters))))) (concept grammar.goal-pattern))
(rule goal_pattern_body silent (seq (optional (seq (ref match_hypothesis) (repeat0 (seq (literal %2C) (ref match_hypothesis))))) (literal %7C-) (capture labeled goal (ref match_pattern))) (concept grammar.goal-pattern-body) (source-names (tree-sitter _goal_pattern_body)))
(rule match_hypothesis normal (seq (ref name) (choice unordered (seq (literal %3A) (ref match_pattern)) (seq (literal %3A%3D) (ref match_pattern)) (seq (literal %3A%3D) (literal %5B) (ref match_pattern) (literal %5D) (literal %3A) (ref match_pattern)))) (concept grammar.match-hypothesis) (source-names (tree-sitter match_hyp)))
(rule match_pattern normal (choice unordered (ref term) (seq (token (seq (literal context) (not (ref word_characters)))) (optional (ref identifier)) (literal %5B) (ref term) (literal %5D))) (concept grammar.match-pattern))
(rule intro_pattern normal (ref intro_pattern_item) (concept grammar.intro-pattern))
(rule intro_pattern_item silent (precedence 0 left (choice unordered (ref identifier) (ref wildcard) (literal %3F) (ref metavariable) (literal -%3E) (literal %3C-) (literal %2A) (literal %2A%2A) (ref bracketed_intro_pattern) (ref parenthesized_intro_pattern) (seq (ref intro_pattern_item) (literal %25) (ref zero_level_term)))) (concept grammar.intro-pattern-item) (source-names (tree-sitter _intro_pattern_item)))
(rule bracketed_intro_pattern normal (seq (literal %5B) (optional (literal %3D)) (repeat0 (choice unordered (ref intro_pattern_item) (literal %7C) (literal %26))) (literal %5D)) (concept grammar.bracketed-intro-pattern))
(rule parenthesized_intro_pattern normal (seq (literal %28) (optional (seq (ref intro_pattern) (repeat0 (seq (choice unordered (literal %2C) (literal %26)) (ref intro_pattern))))) (literal %29)) (concept grammar.parenthesized-intro-pattern))
(rule in_clause normal (precedence 0 right (seq (token (seq (literal in) (not (ref word_characters)))) (choice unordered (seq (ref hypothesis_occurrence) (repeat0 (seq (literal %2C) (ref hypothesis_occurrence))) (optional (ref goal_occurrence))) (seq (literal %2A) (optional (ref goal_occurrence))) (ref goal_occurrence)))) (concept grammar.in-clause))
(rule hypothesis_occurrence silent (precedence 0 right (seq (ref identifier) (optional (ref at_clause)))) (concept grammar.hypothesis-occurrence) (source-names (tree-sitter _hyp_occurrence)))
(rule goal_occurrence silent (precedence 0 right (seq (literal %7C-) (optional (seq (literal %2A) (optional (ref at_clause)))))) (concept grammar.goal-occurrence) (source-names (tree-sitter _goal_occurrence)))
(rule with_clause normal (namedPrecedence tactic_match right (seq (token (seq (literal with) (not (ref word_characters)))) (choice unordered (repeat1 (ref identifier)) (literal %2A)))) (concept grammar.with-clause))
(rule as_clause normal (seq (token (seq (literal as) (not (ref word_characters)))) (repeat1 (ref intro_pattern))) (concept grammar.as-clause))
(rule by_clause normal (precedence 0 right (seq (token (seq (literal by) (not (ref word_characters)))) (ref ltac_expression))) (concept grammar.by-clause))
(rule tactic_bindings normal (namedPrecedence binder right (choice unordered (repeat1 (ref one_term)) (repeat1 (seq (literal %28) (capture labeled name (choice unordered (ref identifier) (ref natural) (ref number))) (literal %3A%3D) (capture labeled value (ref term)) (literal %29))))) (concept grammar.tactic-bindings) (source-names (tree-sitter bindings)))
(rule equation_clause normal (seq (token (seq (literal eqn) (not (ref word_characters)))) (literal %3A) (ref identifier)) (concept grammar.equation-clause) (source-names (tree-sitter eqn_clause)))
(rule using_clause normal (precedence 0 right (seq (token (seq (literal using) (not (ref word_characters)))) (ref one_term) (repeat0 (seq (literal %2C) (ref one_term))))) (concept grammar.using-clause))
(rule qualified_identifier silent (choice unordered (ref identifier) (ref dotted_qualified_identifier)) (concept grammar.qualified-identifier) (source-names (tree-sitter _qualid)))
(rule comment normal (seq (literal %28%2A) (repeat0 (choice unordered (alias unnamed_token (token (repeat1 (class negated (char %2A) (char %28) (char %29))))) (alias unnamed_token (token (class plain (char %2A) (char %28) (char %29)))))) (literal %2A%29)) (concept grammar.comment))
(rule identifier token (seq (class plain (category L) (char _)) (repeat0 (class plain (category L) (char _) (category N) (char %27)))) (concept grammar.identifier) (source-names (tree-sitter ident)))
(rule identifier_declaration normal (ref identifier) (concept grammar.identifier-declaration) (source-names (tree-sitter ident_decl)))
(rule metavariable token (seq (literal %3F) (choice unordered (seq (class plain (range a z) (range A Z) (char _)) (repeat0 (class plain (range a z) (range A Z) (range 0 9) (char _) (char %27)))) (repeat1 (class plain (range 0 9))))) (concept grammar.metavariable))
(rule number token (choice unordered (seq (optional (literal -)) (seq (class plain (range 0 9)) (repeat0 (class plain (range 0 9) (char _)))) (optional (seq (literal .) (repeat1 (class plain (range 0 9) (char _))))) (optional (seq (class plain (char e) (char E)) (optional (class plain (char %2B) (char -))) (seq (class plain (range 0 9)) (repeat0 (class plain (range 0 9) (char _))))))) (seq (optional (literal -)) (seq (literal 0) (class plain (char x) (char X)) (class plain (range 0 9) (range a f) (range A F)) (repeat0 (class plain (range 0 9) (range a f) (range A F) (char _)))) (optional (seq (literal .) (repeat1 (class plain (range 0 9) (range a f) (range A F) (char _))))) (optional (seq (class plain (char p) (char P)) (optional (class plain (char %2B) (char -))) (seq (class plain (range 0 9)) (repeat0 (class plain (range 0 9) (char _)))))))) (concept grammar.number))
(rule integer normal (ref big_integer) (concept grammar.integer-literal))
(rule big_integer silent (seq (optional (literal -)) (ref big_natural_number)) (concept grammar.big-integer) (source-names (tree-sitter _bigint)))
(rule natural silent (ref big_natural_number) (concept grammar.natural) (source-names (tree-sitter _natural)))
(rule big_natural_number silent (choice unordered (ref decimal_natural_number) (ref hexadecimal_natural_number)) (concept grammar.big-natural-number) (source-names (tree-sitter _bignat)))
(rule decimal_natural_number token (seq (class plain (range 0 9)) (repeat0 (class plain (range 0 9) (char _)))) (concept grammar.decimal-natural-number) (source-names (tree-sitter decnat)))
(rule digit token (class plain (range 0 9)) (concept grammar.digit))
(rule hexadecimal_natural_number token (seq (literal 0) (class plain (char x) (char X)) (class plain (range 0 9) (range a f) (range A F)) (repeat0 (class plain (range 0 9) (range a f) (range A F) (char _)))) (concept grammar.hexadecimal-natural-number) (source-names (tree-sitter hexnat)))
(rule hexadecimal_digit token (class plain (range 0 9) (range a f) (range A F)) (concept grammar.hexadecimal-digit) (source-names (tree-sitter hexdigit)))
(rule dotted_qualified_identifier token (seq (seq (class plain (category L) (char _)) (repeat0 (class plain (category L) (char _) (category N) (char %27)))) (repeat0 (seq (literal .) (seq (class plain (category L) (char _)) (repeat0 (class plain (category L) (char _) (category N) (char %27))))))) (concept grammar.dotted-qualified-identifier) (source-names (tree-sitter dotted_qualid)))
(rule annotated_qualified_identifier silent (ref qualified_identifier) (concept grammar.annotated-qualified-identifier) (source-names (tree-sitter _qualid_annotated)))
(rule global_reference normal (choice unordered (ref qualified_identifier) (seq (ref string) (optional (seq (literal %25) (ref identifier))))) (concept grammar.global-reference) (source-names (tree-sitter reference)))
(rule string normal (seq (literal %22) (repeat0 (choice unordered (alias unnamed_token (token (class negated (char %22)))) (literal %22%22))) (literal %22)) (concept grammar.string))
(rule wildcard normal (token (seq (literal _) (not (ref word_characters)))) (concept grammar.wildcard))
(rule custom_notation_block normal (choice unordered (seq (literal %3C%7B) (repeat0 (ref dsl_token)) (literal %7D%3E)) (seq (literal %5B%7C) (repeat0 (ref dsl_token)) (literal %7C%5D)) (seq (literal %7B%7C) (repeat0 (ref dsl_token)) (literal %7C%7D))) (concept grammar.custom-notation-block))
(rule dsl_token silent (choice unordered (ref identifier) (ref number) (ref string) (alias unnamed_token (token (repeat1 (class plain (char %2B) (char -) (char %2A) (char %2F) (char %26) (char %3D) (char %3C) (char %3E) (char %21) (char %7E) (char %7C) (char %25) (char %5E) (char %3A) (char %3B))))) (seq (literal %28) (repeat0 (ref dsl_token)) (literal %29)) (seq (literal %5B) (repeat0 (ref dsl_token)) (literal %5D)) (seq (literal %7B) (repeat0 (ref dsl_token)) (literal %7D))) (concept grammar.dsl-token) (source-names (tree-sitter _dsl_token)))
(rule imp_evaluation_operation normal (namedPrecedence custom left (seq (capture labeled initial_state (ref term)) (literal %3D%5B) (ref imp_program) (literal %5D%3D%3E) (capture labeled final_state (ref term)))) (concept grammar.imp-evaluation-operation))
(rule imp_program normal (repeat1 (ref imp_token)) (concept grammar.imp-program))
(rule imp_token silent (choice unordered (ref identifier) (ref number) (literal %3A%3D) (alias unnamed_token (token (repeat1 (class plain (char %2B) (char -) (char %2A) (char %2F) (char %26) (char %3D) (char %3C) (char %3E) (char %21) (char %7E) (char %7C) (char %25) (char %3B))))) (seq (literal %28) (repeat0 (ref imp_token)) (literal %29)) (seq (literal %5B) (repeat0 (ref imp_token)) (literal %5D)) (seq (literal %7B) (repeat0 (ref imp_token)) (literal %7D))) (concept grammar.imp-token) (source-names (tree-sitter _imp_token)))
(rule word_characters token (seq (class plain (category L) (char _)) (repeat0 (class plain (category L) (char _) (category N) (char %27)))) (concept grammar.word-characters))