(grammar (start module) (matching longest) (settling tokens precedence dynamic ambiguity))
(extra (ref comment))
(extra (class plain (char %20) (char %09) (char %0A) (char %0D) (char %0C) (char %0B)))
(conflict where_declaration)
(conflict subtype field_assignment)
(conflict let pattern)
(conflict parameters pattern)
(conflict have pattern)
(conflict atom name)
(conflict binding_body tactic_have)
(conflict import modifier)
(conflict syntax_atom atom)
(conflict return do_return)
(conflict hash_command explicit)
(scanner layout (tokens layout_start layout_semicolon layout_end match_body_start syntax_quotation_body) (operations (if (some (valid syntax_quotation_body) (expected (ref syntax_quotation_body))) (then (while (not (some atEnd (all (next (literal %29)) (not (greater (depth parens) (integer 0))) (not (greater (depth brackets) (integer 0))) (not (greater (depth braces) (integer 0)))))) (do (if (next (literal %28)) (then (push parens (integer 1)))) (if (next (literal %29)) (then (if (greater (depth parens) (integer 0)) (then (pop parens))))) (if (next (literal %5B)) (then (push brackets (integer 1)))) (if (next (literal %5D)) (then (if (greater (depth brackets) (integer 0)) (then (pop brackets))))) (if (next (literal %7B)) (then (push braces (integer 1)))) (if (next (literal %7D)) (then (if (greater (depth braces) (integer 0)) (then (pop braces))))) advance (if (not (greater (depth consumed) (integer 0))) (then (push consumed (integer 1)))))) (while (greater (depth parens) (integer 0)) (do (pop parens))) (while (greater (depth brackets) (integer 0)) (do (pop brackets))) (while (greater (depth braces) (integer 0)) (do (pop braces))) (if (greater (depth consumed) (integer 0)) (then (pop consumed) mark (emit syntax_quotation_body))) fail)) (if (some (valid layout_start) (expected (ref layout_start))) (then (while (next (class plain (char %20) (char %09))) (do (skip (class plain (char %20) (char %09))))) (if (next (class plain (char %0A) (char %0D))) (then (while (next (class plain (char %0A) (char %0D))) (do (skip (class plain (char %0A) (char %0D))))) (while (next (class plain (char %20) (char %09))) (do (skip (class plain (char %20) (char %09))))) (if atEnd (then (push measured (integer 0))) (else (push measured column))) (if (less (depth indents) (integer 64)) (then (push indents (top measured)))) (pop measured)) (else (if (less (depth indents) (integer 64)) (then (push indents column))))) (if (greater (depth queued) (integer 0)) (then (pop queued))) (emit layout_start))) (if (some (valid match_body_start) (expected (ref match_body_start))) (then (while (next (class plain (char %20) (char %09))) (do (skip (class plain (char %20) (char %09))))) (if (next (class plain (char %0A) (char %0D))) (then (while (next (class plain (char %0A) (char %0D))) (do (skip (class plain (char %0A) (char %0D))))) (while (next (class plain (char %20) (char %09))) (do (skip (class plain (char %20) (char %09))))) (if atEnd (then (push measured (integer 0))) (else (push measured column))) (if (less (depth indents) (integer 64)) (then (push indents (top measured)))) (pop measured)) (else (if (less (depth indents) (integer 64)) (then (push indents column))))) (if (greater (depth queued) (integer 0)) (then (pop queued))) (emit match_body_start))) (if (all (greater (depth queued) (integer 0)) (greater (depth indents) (integer 0))) (then (if (all (less (top queued) (top indents)) (some (valid layout_end) (expected (ref layout_end)))) (then (if (equal (depth indents) (integer 1)) (then mark (while (next (class plain (char %20) (char %09) (char %0A) (char %0D))) (do advance)) (if (next (literal %7C)) (then fail)))) (pop indents) (emit layout_end))) (if (all (equal (top queued) (top indents)) (some (valid layout_semicolon) (expected (ref layout_semicolon)))) (then (while (next (class plain (char %20) (char %09) (char %0A) (char %0D))) (do (skip (class plain (char %20) (char %09) (char %0A) (char %0D))))) (if (next (literal %7C)) (then fail)) (pop queued) (emit layout_semicolon))) (pop queued))) (while (next (class plain (char %20) (char %09))) (do (skip (class plain (char %20) (char %09))))) (if (all (next (class plain (char %0A) (char %0D))) (greater (depth indents) (integer 0))) (then mark (while (next (class plain (char %0A) (char %0D))) (do advance)) (while (next (class plain (char %20) (char %09))) (do advance)) (if atEnd (then (push queued (integer 0))) (else (push queued column))) (if (all (less (top queued) (top indents)) (some (valid layout_end) (expected (ref layout_end)))) (then (if (all (equal (depth indents) (integer 1)) (next (literal %7C))) (then fail)) (pop indents) (emit layout_end))) (if (all (equal (top queued) (top indents)) (some (valid layout_semicolon) (expected (ref layout_semicolon)))) (then (if (next (literal %7C)) (then fail)) (pop queued) (emit layout_semicolon))) fail)) (if (all atEnd (greater (depth indents) (integer 0)) (some (valid layout_end) (expected (ref layout_end)))) (then (pop indents) (emit layout_end))) (if (all (some (valid layout_end) (expected (ref layout_end))) (greater (depth indents) (integer 0)) (some (next (literal %29)) (next (literal %5D)) (next (literal %7D)))) (then (pop indents) (emit layout_end))) fail))
(rule module normal (choice unordered (seq (optional (ref module_header)) (optional (ref prelude)) (repeat0 (ref import)) (repeat0 (ref command))) (repeat1 (ref fragment_element))) (concept grammar.program))
(rule module_header token (seq (literal module) (not (ref word_characters))) (concept grammar.module-header))
(rule fragment_element silent (choice unordered (ref tactic) (ref expression)) (concept grammar.fragment-element) (source-names (tree-sitter _fragment_element)))
(rule prelude token (seq (literal prelude) (not (ref word_characters))) (concept grammar.prelude))
(rule import normal (seq (optional (capture labeled visibility (token (seq (literal public) (not (ref word_characters)))))) (optional (capture labeled meta (token (seq (literal meta) (not (ref word_characters)))))) (token (seq (literal import) (not (ref word_characters)))) (optional (capture labeled all (token (seq (literal all) (not (ref word_characters)))))) (capture labeled module (ref name))) (concept grammar.import))
(rule command silent (choice unordered (seq (repeat0 (ref modifier)) (choice unordered (ref declaration_choice) (ref declaration) (ref example) (ref notation) (ref attribute) (ref initialize))) (ref namespace) (ref section) (ref end) (ref open) (ref export) (ref variable) (ref universe) (ref hash_command) (ref syntax) (ref set_option) (ref include) (ref omit)) (concept grammar.command) (source-names (tree-sitter _command)))
(rule set_option normal (precedence 0 left (seq (token (seq (literal set_option) (not (ref word_characters)))) (capture labeled name (ref name)) (capture labeled value (ref expression)))) (concept grammar.set-option))
(rule modifier silent (choice unordered (token (seq (literal noncomputable) (not (ref word_characters)))) (token (seq (literal partial) (not (ref word_characters)))) (token (seq (literal protected) (not (ref word_characters)))) (token (seq (literal private) (not (ref word_characters)))) (token (seq (literal public) (not (ref word_characters)))) (token (seq (literal meta) (not (ref word_characters)))) (token (seq (literal unsafe) (not (ref word_characters)))) (token (seq (literal scoped) (not (ref word_characters)))) (token (seq (literal local) (not (ref word_characters))))) (concept grammar.modifier) (source-names (tree-sitter _modifier)))
(rule namespace normal (seq (token (seq (literal namespace) (not (ref word_characters)))) (capture labeled name (ref name))) (concept grammar.namespace))
(rule section normal (seq (optional (capture labeled visibility (token (seq (literal public) (not (ref word_characters)))))) (token (seq (literal section) (not (ref word_characters)))) (optional (capture labeled name (ref name)))) (concept grammar.section-command))
(rule end normal (seq (token (seq (literal end) (not (ref word_characters)))) (optional (capture labeled name (ref name)))) (concept grammar.end-command))
(rule syntax normal (seq (token (seq (literal syntax) (not (ref word_characters)))) (optional (seq (literal %28) (choice unordered (token (seq (literal name) (not (ref word_characters)))) (token (seq (literal priority) (not (ref word_characters))))) (literal %3A%3D) (capture labeled attr (ref expression)) (literal %29))) (repeat1 (capture labeled kind (ref syntax_atom))) (literal %3A) (capture labeled category (ref identifier))) (concept grammar.syntax))
(rule syntax_atom silent (choice unordered (ref string) (ref identifier) (ref number) (ref syntax_group)) (concept grammar.syntax-atom) (source-names (tree-sitter _syntax_atom)))
(rule syntax_group normal (seq (literal %28) (repeat1 (ref syntax_atom)) (literal %29) (optional (capture labeled quantifier (choice unordered (literal %3F) (literal %2A) (literal %2B))))) (concept grammar.syntax-group))
(rule initialize normal (seq (choice unordered (token (seq (literal initialize) (not (ref word_characters)))) (token (seq (literal builtin_initialize) (not (ref word_characters))))) (optional (seq (capture labeled name (ref identifier)) (literal %3A) (capture labeled type (ref expression)) (literal %E2%86%90))) (capture labeled value (ref expression))) (concept grammar.initialization-command))
(rule open normal (seq (token (seq (literal open) (not (ref word_characters)))) (optional (token (seq (literal scoped) (not (ref word_characters))))) (repeat1 (capture labeled namespace (ref name))) (optional (choice unordered (seq (token (seq (literal hiding) (not (ref word_characters)))) (repeat1 (capture labeled hiding (ref name)))) (seq (literal %28) (repeat1 (capture labeled only (ref name))) (literal %29)) (seq (token (seq (literal in) (not (ref word_characters)))) (ref command))))) (concept grammar.open))
(rule export normal (seq (token (seq (literal export) (not (ref word_characters)))) (capture labeled class (ref identifier)) (literal %28) (repeat0 (ref identifier)) (literal %29)) (concept grammar.export))
(rule variable normal (seq (token (seq (literal variable) (not (ref word_characters)))) (repeat1 (ref bracketed_binder))) (concept grammar.variable-command))
(rule universe normal (seq (choice unordered (token (seq (literal universe) (not (ref word_characters)))) (token (seq (literal universes) (not (ref word_characters))))) (repeat1 (ref identifier))) (concept grammar.universe))
(rule include normal (seq (token (seq (literal include) (not (ref word_characters)))) (repeat1 (capture labeled name (ref identifier)))) (concept grammar.include-command))
(rule omit normal (seq (token (seq (literal omit) (not (ref word_characters)))) (repeat1 (capture labeled name (ref identifier)))) (concept grammar.omit-command))
(rule attribute normal (precedence 0 left (seq (token (seq (literal attribute) (not (ref word_characters)))) (literal %5B) (seq (ref identifier) (repeat0 (seq (literal %2C) (ref identifier)))) (literal %5D) (repeat1 (ref expression)))) (concept grammar.attribute-command))
(rule notation normal (precedence 0 left (seq (choice unordered (token (seq (literal notation) (not (ref word_characters)))) (token (seq (literal macro_rules) (not (ref word_characters)))) (token (seq (literal syntax) (not (ref word_characters)))) (token (seq (literal macro) (not (ref word_characters)))) (token (seq (literal elab) (not (ref word_characters)))) (token (seq (literal prefix) (not (ref word_characters)))) (token (seq (literal infix) (not (ref word_characters)))) (token (seq (literal infixl) (not (ref word_characters)))) (token (seq (literal infixr) (not (ref word_characters)))) (token (seq (literal postfix) (not (ref word_characters))))) (optional (seq (literal %3A) (ref number))) (repeat0 (choice unordered (ref expression) (literal %3D%3E) (literal %3A%3D))))) (concept grammar.notation))
(rule hash_command normal (precedence 0 left (seq (alias unnamed_token (token (seq (literal %23) (class plain (range a z) (range A Z) (char _)) (repeat0 (class plain (range a z) (range A Z) (range 0 9) (char _)))))) (repeat0 (ref expression)))) (concept grammar.hash-command))
(rule example normal (seq (token (seq (literal example) (not (ref word_characters)))) (optional (capture labeled binders (ref binders))) (optional (ref type_specification)) (literal %3A%3D) (capture labeled body (ref expression))) (concept grammar.example))
(rule declaration_choice silent (choice unordered (ref definition) (alias definition (ref instance_declaration)) (ref constant) (ref opaque) (ref axiom) (ref structure) (ref inductive) (ref class_inductive)) (concept grammar.declaration-choice) (source-names (tree-sitter _declaration)))
(rule declaration normal (seq (capture labeled attributes (ref attributes)) (repeat0 (ref modifier)) (ref declaration_choice)) (concept grammar.declaration))
(rule attributes normal (seq (literal %40) (literal %5B) (seq (ref attribute_entry) (repeat0 (seq (literal %2C) (ref attribute_entry)))) (literal %5D)) (concept grammar.attribute-list))
(rule attribute_entry normal (seq (capture labeled name (ref name)) (repeat0 (capture labeled arg (choice unordered (ref identifier) (ref escaped_identifier) (ref string) (ref number))))) (concept grammar.attribute-entry))
(rule definition normal (seq (capture labeled kind (choice unordered (token (seq (literal def) (not (ref word_characters)))) (token (seq (literal theorem) (not (ref word_characters)))) (token (seq (literal lemma) (not (ref word_characters)))) (token (seq (literal abbrev) (not (ref word_characters)))))) (capture labeled name (ref name)) (optional (capture labeled binders (ref binders))) (optional (ref type_specification)) (ref declaration_body)) (concept grammar.definition))
(rule declaration_body silent (choice unordered (seq (literal %3A%3D) (alias unnamed_token (immediateToken (ref layout_start))) (capture labeled body (ref expression)) (optional (alias unnamed_token (immediateToken (ref layout_end))))) (seq (token (seq (literal where) (not (ref word_characters)))) (alias unnamed_token (immediateToken (ref layout_start))) (repeat1 (seq (capture labeled body (ref where_declaration)) (optional (alias unnamed_token (immediateToken (ref layout_semicolon)))))) (optional (alias unnamed_token (immediateToken (ref layout_end))))) (repeat1 (ref match_arm))) (concept grammar.declaration-body) (source-names (tree-sitter _declaration_body)))
(rule instance_declaration silent (seq (token (seq (literal instance) (not (ref word_characters)))) (optional (capture labeled name (ref identifier))) (repeat0 (capture labeled binders (ref bracketed_binder))) (optional (ref type_specification)) (ref declaration_body)) (concept grammar.instance-declaration) (source-names (tree-sitter _instance_decl)))
(rule where_declaration normal (seq (capture labeled name (ref identifier)) (repeat0 (capture labeled binders (choice unordered (ref identifier) (ref bracketed_binder)))) (optional (ref type_specification)) (choice unordered (seq (literal %3A%3D) (alias unnamed_token (immediateToken (ref layout_start))) (capture labeled body (ref expression)) (optional (alias unnamed_token (immediateToken (ref layout_end))))) (repeat1 (ref match_arm)))) (concept grammar.where-declaration) (source-names (tree-sitter where_decl)))
(rule constant normal (seq (token (seq (literal constant) (not (ref word_characters)))) (capture labeled name (ref name)) (optional (ref type_specification)) (optional (seq (literal %3A%3D) (capture labeled body (ref expression))))) (concept grammar.constant))
(rule opaque normal (seq (token (seq (literal opaque) (not (ref word_characters)))) (capture labeled name (ref name)) (optional (capture labeled binders (ref binders))) (optional (ref type_specification)) (optional (seq (literal %3A%3D) (capture labeled body (ref expression))))) (concept grammar.opaque-declaration))
(rule axiom normal (seq (token (seq (literal axiom) (not (ref word_characters)))) (capture labeled name (ref name)) (ref type_specification)) (concept grammar.axiom))
(rule structure normal (seq (choice unordered (token (seq (literal structure) (not (ref word_characters)))) (token (seq (literal class) (not (ref word_characters))))) (capture labeled name (ref identifier)) (optional (capture labeled binders (ref binders))) (optional (capture labeled extends (seq (token (seq (literal extends) (not (ref word_characters)))) (seq (ref expression) (repeat0 (seq (literal %2C) (ref expression))))))) (optional (ref type_specification)) (optional (seq (choice unordered (literal %3A%3D) (token (seq (literal where) (not (ref word_characters))))) (alias unnamed_token (immediateToken (ref layout_start))) (repeat0 (seq (capture labeled fields (choice unordered (ref structure_field) (ref bracketed_binder))) (optional (alias unnamed_token (immediateToken (ref layout_semicolon)))))) (optional (alias unnamed_token (immediateToken (ref layout_end)))))) (optional (seq (token (seq (literal deriving) (not (ref word_characters)))) (seq (capture labeled deriving (ref identifier)) (repeat0 (seq (literal %2C) (capture labeled deriving (ref identifier)))))))) (concept grammar.structure))
(rule structure_field normal (seq (capture labeled name (ref identifier)) (repeat0 (ref bracketed_binder)) (choice unordered (seq (literal %3A) (capture labeled type (ref expression)) (optional (seq (literal %3A%3D) (capture labeled default (ref expression))))) (seq (literal %3A%3D) (capture labeled default (ref expression))))) (concept grammar.structure-field))
(rule inductive normal (seq (token (seq (literal inductive) (not (ref word_characters)))) (capture labeled name (ref identifier)) (optional (capture labeled binders (ref binders))) (optional (ref type_specification)) (optional (choice unordered (literal %3A%3D) (token (seq (literal where) (not (ref word_characters)))))) (repeat0 (capture labeled constructors (ref constructor))) (optional (seq (token (seq (literal deriving) (not (ref word_characters)))) (seq (capture labeled deriving (ref identifier)) (repeat0 (seq (literal %2C) (capture labeled deriving (ref identifier)))))))) (concept grammar.inductive-declaration))
(rule class_inductive normal (precedence 1 none (seq (token (seq (literal class) (not (ref word_characters)))) (token (seq (literal inductive) (not (ref word_characters)))) (capture labeled name (ref identifier)) (optional (capture labeled binders (ref binders))) (optional (ref type_specification)) (optional (choice unordered (literal %3A%3D) (token (seq (literal where) (not (ref word_characters)))))) (repeat0 (capture labeled constructors (ref constructor))) (optional (seq (token (seq (literal deriving) (not (ref word_characters)))) (seq (capture labeled deriving (ref identifier)) (repeat0 (seq (literal %2C) (capture labeled deriving (ref identifier))))))))) (concept grammar.class-inductive-declaration))
(rule constructor normal (seq (literal %7C) (capture labeled name (ref name)) (optional (capture labeled binders (ref binders))) (optional (ref type_specification))) (concept grammar.constructor))
(rule binders normal (repeat1 (choice unordered (ref identifier) (ref bracketed_binder))) (concept grammar.binders))
(rule quantifier_binders silent (seq (repeat1 (choice unordered (ref identifier) (ref bracketed_binder))) (optional (ref type_specification))) (concept grammar.quantifier-binders) (source-names (tree-sitter _quantifier_binders)))
(rule bracketed_binder silent (choice unordered (ref explicit_binder) (ref implicit_binder) (ref instance_binder)) (concept grammar.bracketed-binder) (source-names (tree-sitter _bracketed_binder)))
(rule explicit_binder normal (seq (literal %28) (repeat1 (capture labeled name (ref identifier))) (optional (ref type_specification)) (optional (seq (literal %3A%3D) (capture labeled default (ref expression)))) (literal %29)) (concept grammar.explicit-binder))
(rule implicit_binder normal (seq (literal %7B) (repeat1 (capture labeled name (ref identifier))) (optional (ref type_specification)) (literal %7D)) (concept grammar.implicit-binder))
(rule instance_binder normal (seq (literal %5B) (optional (seq (capture labeled name (ref identifier)) (literal %3A))) (capture labeled type (ref expression)) (literal %5D)) (concept grammar.instance-binder))
(rule type_specification silent (seq (literal %3A) (capture labeled type (ref expression))) (concept grammar.type-specification) (source-names (tree-sitter _type_spec)))
(rule expression silent (choice unordered (ref atom) (ref application) (ref subscript) (ref binary_expression) (ref unary_expression) (ref explicit) (ref projection) (ref arrow) (ref fun) (ref quantifier) (ref let) (ref have) (ref if) (ref if_let) (ref match) (ref do) (ref by) (ref try) (ref return) (ref as_pattern)) (concept grammar.expression) (source-names (tree-sitter _expression)))
(rule try normal (precedence 0 right (seq (token (seq (literal try) (not (ref word_characters)))) (alias unnamed_token (immediateToken (ref layout_start))) (capture labeled body (ref do_sequence)) (optional (alias unnamed_token (immediateToken (ref layout_end)))) (token (seq (literal catch) (not (ref word_characters)))) (optional (capture labeled var (choice unordered (ref identifier) (ref hole)))) (literal %3D%3E) (alias unnamed_token (immediateToken (ref layout_start))) (capture labeled handler (ref do_sequence)) (optional (alias unnamed_token (immediateToken (ref layout_end)))))) (concept grammar.try))
(rule return normal (precedence 0 right (seq (token (seq (literal return) (not (ref word_characters)))) (optional (capture labeled value (ref expression))))) (concept grammar.return-expression))
(rule as_pattern normal (seq (capture labeled binder (ref identifier)) (immediateToken (literal %40)) (capture labeled pattern (ref atom))) (concept grammar.as-pattern))
(rule atom silent (choice unordered (ref identifier) (ref escaped_identifier) (ref number) (ref float) (ref string) (ref interpolated_string) (ref character) (ref parenthesized) (ref named_argument) (ref tuple) (ref anonymous_constructor) (ref structure_instance) (ref array) (ref list) (ref range) (ref hole) (ref synthetic_hole) (ref quoted_name) (ref double_quoted_name) (ref syntax_quotation) (ref ellipsis) (ref sorry) (ref boolean) (ref centered_dot) (ref subtype)) (concept grammar.atom) (source-names (tree-sitter _atom)))
(rule application normal (precedence 80 left (seq (capture labeled name (ref expression)) (capture labeled arguments (choice unordered (ref atom) (ref fun) (ref if) (ref match) (ref do) (ref by))))) (concept grammar.function-application))
(rule subscript normal (precedence 90 left (seq (capture labeled object (ref expression)) (immediateToken (literal %5B)) (optional (capture labeled index (ref expression))) (optional (seq (literal %3A) (optional (capture labeled stop (ref expression))))) (literal %5D) (optional (capture labeled modifier (choice unordered (literal %21) (literal %3F)))))) (concept grammar.subscript))
(rule name silent (precedence 0 right (seq (choice unordered (ref identifier) (ref escaped_identifier)) (repeat0 (seq (immediateToken (literal .)) (choice unordered (ref identifier) (ref escaped_identifier)))))) (concept grammar.name) (source-names (tree-sitter _name)))
(rule projection normal (precedence 90 left (seq (optional (capture labeled term (ref expression))) (choice unordered (immediateToken (literal .)) (literal .)) (capture labeled name (choice unordered (ref identifier) (ref escaped_identifier) (ref number))))) (concept grammar.projection))
(rule arrow normal (precedence 25 right (seq (capture labeled domain (ref expression)) (choice unordered (literal -%3E) (literal %E2%86%92)) (capture labeled codomain (ref expression)))) (concept grammar.arrow))
(rule binary_expression normal (choice unordered (precedence 25 left (seq (capture labeled left (ref expression)) (capture labeled operator (choice unordered (literal %7C%7C) (literal %E2%88%A8) (literal %3C%7C%3E) (literal %3C%24%3E) (literal %3C%2A%3E) (literal %2A%3E) (literal %3C%2A))) (capture labeled right (ref expression)))) (precedence 35 left (seq (capture labeled left (ref expression)) (capture labeled operator (choice unordered (literal %26%26) (literal %E2%88%A7))) (capture labeled right (ref expression)))) (precedence 40 left (seq (capture labeled left (ref expression)) (capture labeled operator (choice unordered (literal %3D%3D) (literal %21%3D) (literal %3D) (literal %3C) (literal %3E) (literal %3C%3D) (literal %3E%3D) (literal %E2%89%A4) (literal %E2%89%A5) (literal %E2%89%A0) (literal %E2%88%A3) (literal %E2%86%94) (literal %E2%8A%A2))) (capture labeled right (ref expression)))) (precedence 55 left (seq (capture labeled left (ref expression)) (capture labeled operator (choice unordered (literal %2B) (literal -) (literal %2B%2B) (literal %E2%88%AA) (literal %E2%88%A9) (literal %C3%97) (literal %5C))) (capture labeled right (ref expression)))) (precedence 60 left (seq (capture labeled left (ref expression)) (capture labeled operator (choice unordered (literal %2A) (literal %2F) (literal %25))) (capture labeled right (ref expression)))) (precedence 81 left (seq (capture labeled left (ref expression)) (capture labeled operator (choice unordered (literal %7C%3E) (literal %7C%3E.))) (capture labeled right (ref expression)))) (precedence 25 right (seq (capture labeled left (ref expression)) (capture labeled operator (literal %24)) (capture labeled right (ref expression)))) (precedence 55 right (seq (capture labeled left (ref expression)) (capture labeled operator (literal %3A%3A)) (capture labeled right (ref expression)))) (precedence 60 right (seq (capture labeled left (ref expression)) (capture labeled operator (choice unordered (literal %5E) (literal %E2%88%98))) (capture labeled right (ref expression)))) (precedence 81 right (seq (capture labeled left (ref expression)) (capture labeled operator (literal %3C%7C)) (capture labeled right (ref expression))))) (concept grammar.binary-expression))
(rule unary_expression normal (precedence 70 none (seq (capture labeled operator (choice unordered (literal %21) (literal %C2%AC) (literal -) (literal %E2%86%90) (literal %3C-))) (capture labeled operand (ref expression)))) (concept grammar.unary-expression))
(rule explicit normal (seq (literal %40) (ref atom)) (concept grammar.explicit-term))
(rule fun normal (precedence 0 right (seq (choice unordered (token (seq (literal fun) (not (ref word_characters)))) (token (seq (literal %CE%BB) (not (ref word_characters))))) (choice unordered (seq (capture labeled binders (repeat1 (choice unordered (ref pattern) (ref bracketed_binder)))) (literal %3D%3E) (alias unnamed_token (immediateToken (ref layout_start))) (capture labeled body (ref expression)) (optional (alias unnamed_token (immediateToken (ref layout_end))))) (repeat1 (ref match_arm))))) (concept grammar.fun))
(rule quantifier normal (precedence 0 right (seq (capture labeled quantifier (choice unordered (token (seq (literal forall) (not (ref word_characters)))) (literal %E2%88%80) (token (seq (literal exists) (not (ref word_characters)))) (literal %E2%88%83))) (ref quantifier_tail))) (concept grammar.quantifier))
(rule quantifier_tail silent (seq (capture labeled binders (ref quantifier_binders)) (literal %2C) (capture labeled body (ref expression))) (concept grammar.quantifier-tail) (source-names (tree-sitter _quantifier_tail)))
(rule have normal (precedence 0 right (seq (token (seq (literal have) (not (ref word_characters)))) (optional (capture labeled name (ref identifier))) (optional (ref type_specification)) (ref binding_body))) (concept grammar.have))
(rule binding_body silent (precedence 0 right (seq (literal %3A%3D) (capture labeled value (ref expression)) (optional (seq (choice unordered (literal %3B) (alias unnamed_token (immediateToken (ref layout_semicolon)))) (capture labeled body (ref expression)))))) (concept grammar.binding-body) (source-names (tree-sitter _binding_body)))
(rule by normal (precedence 0 right (seq (token (seq (literal by) (not (ref word_characters)))) (alias unnamed_token (immediateToken (ref layout_start))) (ref tactic_sequence) (optional (alias unnamed_token (immediateToken (ref layout_end)))))) (concept grammar.tactic-proof))
(rule tactic_sequence silent (precedence 0 right (seq (ref tactic) (repeat0 (seq (choice unordered (alias unnamed_token (immediateToken (ref layout_semicolon))) (literal %3B) (literal %3C%3B%3E) (literal %3C%3B)) (ref tactic))) (optional (literal %3B)))) (concept grammar.tactic-sequence) (source-names (tree-sitter _tactic_seq)))
(rule tactic silent (choice unordered (ref tactic_apply) (ref tactic_focus) (ref tactic_case) (ref tactic_rewrite) (ref tactic_have) (ref tactic_let) (ref tactic_show) (ref tactic_calculation)) (concept grammar.tactic) (source-names (tree-sitter _tactic)))
(rule tactic_apply normal (precedence 80 right (seq (capture labeled tactic (ref identifier)) (repeat0 (capture labeled arg (choice unordered (ref expression) (ref tactic_configuration)))))) (concept grammar.apply-tactic))
(rule tactic_configuration normal (precedence 1 none (seq (literal %5B) (optional (seq (ref expression) (repeat0 (seq (literal %2C) (ref expression))))) (literal %5D))) (concept grammar.tactic-configuration) (source-names (tree-sitter tactic_config)))
(rule tactic_focus normal (precedence 0 right (seq (literal %C2%B7) (alias unnamed_token (immediateToken (ref layout_start))) (ref tactic_sequence) (optional (alias unnamed_token (immediateToken (ref layout_end)))))) (concept grammar.tactic-focus))
(rule tactic_case normal (precedence 0 right (seq (choice unordered (token (seq (literal case) (not (ref word_characters)))) (token (seq (literal next) (not (ref word_characters))))) (repeat0 (ref identifier)) (literal %3D%3E) (alias unnamed_token (immediateToken (ref layout_start))) (ref tactic_sequence) (optional (alias unnamed_token (immediateToken (ref layout_end)))))) (concept grammar.tactic-case))
(rule tactic_rewrite normal (precedence 80 right (seq (choice unordered (token (seq (literal rw) (not (ref word_characters)))) (token (seq (literal rewrite) (not (ref word_characters))))) (choice unordered (ref tactic_configuration) (repeat1 (capture labeled arg (ref expression)))) (optional (seq (token (seq (literal at) (not (ref word_characters)))) (repeat1 (choice unordered (ref identifier) (literal %2A))))))) (concept grammar.tactic-rewrite))
(rule tactic_have normal (precedence 0 right (seq (choice unordered (token (seq (literal have) (not (ref word_characters)))) (token (seq (literal obtain) (not (ref word_characters)))) (token (seq (literal suffices) (not (ref word_characters))))) (optional (capture labeled name (ref pattern))) (optional (ref type_specification)) (literal %3A%3D) (capture labeled value (ref expression)))) (concept grammar.tactic-have))
(rule tactic_let normal (precedence 1 none (seq (token (seq (literal let) (not (ref word_characters)))) (capture labeled pattern (ref pattern)) (optional (ref type_specification)) (literal %3A%3D) (capture labeled value (ref expression)))) (concept grammar.tactic-let))
(rule tactic_show normal (seq (token (seq (literal show) (not (ref word_characters)))) (ref expression)) (concept grammar.tactic-show))
(rule tactic_calculation normal (precedence 0 right (seq (token (seq (literal calc) (not (ref word_characters)))) (alias unnamed_token (immediateToken (ref layout_start))) (repeat1 (ref calculation_step)) (optional (alias unnamed_token (immediateToken (ref layout_end)))))) (concept grammar.tactic-calculation) (source-names (tree-sitter tactic_calc)))
(rule calculation_step normal (precedence 0 right (seq (ref expression) (literal %3A%3D) (ref expression))) (concept grammar.calculation-step) (source-names (tree-sitter calc_step)))
(rule let normal (precedence 0 right (choice unordered (seq (token (seq (literal let) (not (ref word_characters)))) (capture labeled name (ref identifier)) (optional (capture labeled parameters (ref parameters))) (optional (ref type_specification)) (ref binding_body)) (seq (token (seq (literal let) (not (ref word_characters)))) (capture labeled pattern (choice unordered (ref tuple_pattern) (ref hole))) (optional (ref type_specification)) (ref binding_body)))) (concept grammar.let))
(rule parameters normal (repeat1 (choice unordered (ref identifier) (ref bracketed_binder))) (concept grammar.parameter-binders))
(rule if normal (precedence 0 right (seq (token (seq (literal if) (not (ref word_characters)))) (optional (seq (capture labeled hyp (ref identifier)) (literal %3A))) (capture labeled condition (ref expression)) (ref then_else))) (concept grammar.if-expression))
(rule then_else silent (precedence 0 right (seq (token (seq (literal then) (not (ref word_characters)))) (capture labeled then (ref expression)) (optional (seq (token (seq (literal else) (not (ref word_characters)))) (capture labeled else (ref expression)))))) (concept grammar.then-else-branches) (source-names (tree-sitter _then_else)))
(rule if_let normal (precedence 0 right (seq (token (seq (literal if) (not (ref word_characters)))) (token (seq (literal let) (not (ref word_characters)))) (capture labeled pattern (ref pattern)) (choice unordered (literal %3A%3D) (literal %3C-) (literal %E2%86%90)) (capture labeled value (ref expression)) (ref then_else))) (concept grammar.if-let))
(rule pattern silent (choice unordered (ref identifier) (ref hole) (ref tuple_pattern) (ref constructor_pattern) (ref syntax_quotation)) (concept grammar.pattern) (source-names (tree-sitter _pattern)))
(rule tuple_pattern normal (seq (literal %28) (ref pattern) (literal %2C) (seq (ref pattern) (repeat0 (seq (literal %2C) (ref pattern)))) (literal %29)) (concept grammar.tuple-pattern))
(rule list_pattern normal (seq (literal %5B) (seq (ref pattern) (repeat0 (seq (literal %2C) (ref pattern)))) (literal %5D)) (concept grammar.list-pattern))
(rule constructor_pattern normal (precedence 80 left (seq (capture labeled constructor (ref identifier)) (repeat1 (capture labeled arg (ref pattern))))) (concept grammar.constructor-pattern))
(rule match normal (precedence 0 right (seq (token (seq (literal match) (not (ref word_characters)))) (capture labeled scrutinees (seq (ref expression) (repeat0 (seq (literal %2C) (ref expression))))) (token (seq (literal with) (not (ref word_characters)))) (repeat1 (ref match_arm)))) (concept grammar.match-expression))
(rule match_arm normal (precedence 0 right (seq (literal %7C) (capture labeled patterns (seq (ref expression) (repeat0 (seq (literal %2C) (ref expression))))) (literal %3D%3E) (alias unnamed_token (immediateToken (ref match_body_start))) (capture labeled body (ref expression)) (optional (alias unnamed_token (immediateToken (ref layout_end)))))) (concept grammar.match-arm))
(rule do normal (precedence 0 right (seq (token (seq (literal do) (not (ref word_characters)))) (alias unnamed_token (immediateToken (ref layout_start))) (ref do_sequence) (optional (alias unnamed_token (immediateToken (ref layout_end)))))) (concept grammar.do))
(rule do_sequence silent (precedence 0 right (seq (ref do_element) (repeat0 (seq (choice unordered (alias unnamed_token (immediateToken (ref layout_semicolon))) (literal %3B)) (ref do_element))))) (concept grammar.do-sequence) (source-names (tree-sitter _do_seq)))
(rule do_element silent (choice unordered (ref do_let) (ref let_bind) (ref let_mutable) (ref reassign) (ref do_return) (ref for_in) (ref do_while) (ref do_unless) (ref do_debug_trace) (ref do_break) (ref do_continue) (ref do_if) (ref do_if_let) (ref do_match) (ref expression)) (concept grammar.do-element) (source-names (tree-sitter _do_element)))
(rule do_let normal (precedence 2 right (seq (token (seq (literal let) (not (ref word_characters)))) (capture labeled pattern (choice unordered (ref pattern) (ref list_pattern))) (optional (ref type_specification)) (literal %3A%3D) (capture labeled value (ref expression)) (optional (seq (literal %7C) (capture labeled fallback (ref expression)))))) (concept grammar.do-let))
(rule let_bind normal (seq (token (seq (literal let) (not (ref word_characters)))) (capture labeled name (ref pattern)) (optional (ref type_specification)) (choice unordered (literal %3C-) (literal %E2%86%90)) (capture labeled value (ref expression))) (concept grammar.let-bind))
(rule let_mutable normal (seq (token (seq (literal let) (not (ref word_characters)))) (token (seq (literal mut) (not (ref word_characters)))) (capture labeled name (ref identifier)) (optional (ref type_specification)) (choice unordered (literal %3C-) (literal %E2%86%90) (literal %3A%3D)) (capture labeled value (ref expression))) (concept grammar.mutable-let-binding) (source-names (tree-sitter let_mut)))
(rule reassign normal (precedence 1 right (seq (capture labeled name (ref identifier)) (literal %3A%3D) (capture labeled value (ref expression)))) (concept grammar.reassignment))
(rule do_return normal (precedence 0 right (seq (token (seq (literal return) (not (ref word_characters)))) (optional (capture labeled value (ref expression))))) (concept grammar.do-return))
(rule for_in normal (precedence 81 right (seq (token (seq (literal for) (not (ref word_characters)))) (ref for_binding) (repeat0 (seq (literal %2C) (ref for_binding))) (capture labeled body (ref do)))) (concept grammar.for-in-loop))
(rule for_binding silent (seq (capture labeled var (choice unordered (ref pattern) (ref structure_instance))) (token (seq (literal in) (not (ref word_characters)))) (capture labeled iterable (precedence 81 none (ref expression)))) (concept grammar.for-binding) (source-names (tree-sitter _for_binding)))
(rule do_if normal (precedence 1 right (seq (token (seq (literal if) (not (ref word_characters)))) (optional (seq (capture labeled hyp (ref identifier)) (literal %3A))) (capture labeled condition (ref expression)) (ref do_then_else))) (concept grammar.do-if-statement))
(rule do_then_else silent (precedence 0 right (seq (token (seq (literal then) (not (ref word_characters)))) (alias unnamed_token (immediateToken (ref layout_start))) (capture labeled then (ref do_sequence)) (optional (alias unnamed_token (immediateToken (ref layout_end)))) (optional (seq (token (seq (literal else) (not (ref word_characters)))) (alias unnamed_token (immediateToken (ref layout_start))) (capture labeled else (ref do_sequence)) (optional (alias unnamed_token (immediateToken (ref layout_end)))))))) (concept grammar.do-then-else-branches) (source-names (tree-sitter _do_then_else)))
(rule do_if_let normal (precedence 1 right (seq (token (seq (literal if) (not (ref word_characters)))) (token (seq (literal let) (not (ref word_characters)))) (capture labeled pattern (ref pattern)) (choice unordered (literal %3A%3D) (literal %3C-) (literal %E2%86%90)) (capture labeled value (ref expression)) (ref do_then_else))) (concept grammar.do-if-let))
(rule do_match normal (precedence 1 left (seq (token (seq (literal match) (not (ref word_characters)))) (capture labeled scrutinees (seq (ref expression) (repeat0 (seq (literal %2C) (ref expression))))) (token (seq (literal with) (not (ref word_characters)))) (repeat1 (ref do_match_arm)))) (concept grammar.do-match))
(rule do_match_arm normal (precedence 0 right (seq (literal %7C) (capture labeled patterns (seq (ref expression) (repeat0 (seq (literal %2C) (ref expression))))) (literal %3D%3E) (alias unnamed_token (immediateToken (ref layout_start))) (capture labeled body (ref do_sequence)) (optional (alias unnamed_token (immediateToken (ref layout_end)))))) (concept grammar.do-match-arm))
(rule do_while normal (precedence 1 right (seq (token (seq (literal while) (not (ref word_characters)))) (capture labeled condition (ref expression)) (capture labeled body (ref do)))) (concept grammar.do-while))
(rule do_unless normal (precedence 1 right (seq (token (seq (literal unless) (not (ref word_characters)))) (capture labeled condition (ref expression)) (capture labeled body (ref do)))) (concept grammar.do-unless-statement))
(rule do_debug_trace normal (precedence 0 right (seq (token (seq (literal dbg_trace) (not (ref word_characters)))) (capture labeled value (ref expression)))) (concept grammar.do-debug-trace) (source-names (tree-sitter do_dbg_trace)))
(rule do_break token (seq (literal break) (not (ref word_characters))) (concept grammar.do-break))
(rule do_continue token (seq (literal continue) (not (ref word_characters))) (concept grammar.do-continue-statement))
(rule do_try normal (precedence 0 right (seq (token (seq (literal try) (not (ref word_characters)))) (alias unnamed_token (immediateToken (ref layout_start))) (capture labeled body (ref do_sequence)) (optional (alias unnamed_token (immediateToken (ref layout_end)))))) (concept grammar.do-try))
(rule do_catch normal (precedence 0 right (seq (token (seq (literal catch) (not (ref word_characters)))) (optional (capture labeled var (ref identifier))) (literal %3D%3E) (capture labeled handler (ref expression)))) (concept grammar.do-catch-clause))
(rule parenthesized normal (seq (literal %28) (optional (seq (ref expression) (optional (seq (literal %3A) (capture labeled type (ref expression)))))) (literal %29)) (concept grammar.parenthesized-expression))
(rule named_argument normal (seq (literal %28) (capture labeled name (ref identifier)) (literal %3A%3D) (capture labeled value (ref expression)) (literal %29)) (concept grammar.named-argument))
(rule tuple normal (seq (literal %28) (ref expression) (literal %2C) (seq (ref expression) (repeat0 (seq (literal %2C) (ref expression)))) (literal %29)) (concept grammar.tuple-expression))
(rule anonymous_constructor normal (seq (literal %E2%9F%A8) (optional (seq (ref expression) (repeat0 (seq (literal %2C) (ref expression))))) (literal %E2%9F%A9)) (concept grammar.anonymous-constructor))
(rule subtype normal (seq (literal %7B) (capture labeled var (ref identifier)) (optional (ref type_specification)) (literal %2F%2F) (capture labeled property (ref expression)) (literal %7D)) (concept grammar.subtype))
(rule structure_instance normal (seq (literal %7B) (optional (ref structure_body)) (literal %7D)) (concept grammar.structure-instance))
(rule structure_body silent (choice unordered (seq (capture labeled extends (ref expression)) (token (seq (literal with) (not (ref word_characters)))) (optional (seq (choice unordered (ref field_assignment) (ref ellipsis)) (repeat0 (seq (choice unordered (literal %2C) (alias unnamed_token (token (literal %0A)))) (choice unordered (ref field_assignment) (ref ellipsis)))))) (optional (ref type_specification))) (seq (choice unordered (ref field_assignment) (ref ellipsis)) (repeat0 (seq (choice unordered (literal %2C) (alias unnamed_token (token (literal %0A)))) (choice unordered (ref field_assignment) (ref ellipsis)))) (optional (ref type_specification))) (ref type_specification)) (concept grammar.structure-body) (source-names (tree-sitter _structure_body)))
(rule field_assignment normal (choice unordered (seq (capture labeled name (ref identifier)) (literal %3A%3D) (capture labeled value (ref expression))) (capture labeled name (ref identifier))) (concept grammar.field-assignment))
(rule array normal (seq (literal %23%5B) (optional (seq (ref expression) (repeat0 (seq (literal %2C) (ref expression))))) (literal %5D)) (concept grammar.array))
(rule list normal (seq (literal %5B) (optional (seq (ref expression) (repeat0 (seq (literal %2C) (ref expression))))) (literal %5D)) (concept grammar.list))
(rule range normal (seq (literal %5B) (ref range_specification) (literal %5D)) (concept grammar.index-range))
(rule range_specification silent (seq (optional (capture labeled start (ref expression))) (literal %3A) (optional (capture labeled end (ref expression))) (optional (seq (literal %3A) (capture labeled step (ref expression))))) (concept grammar.range-specification) (source-names (tree-sitter _range_spec)))
(rule identifier token (seq (class plain (char _) (range a z) (range A Z) (range %CE%B1 %CF%89) (range %CE%91 %CE%A9) (char %E2%84%95) (char %E2%84%A4) (char %E2%84%9A) (char %E2%84%9D) (char %E2%84%82) (char %E2%88%87)) (repeat0 (class plain (char _) (range a z) (range A Z) (range 0 9) (char %27) (range %CE%B1 %CF%89) (range %CE%91 %CE%A9) (char %E2%84%95) (char %E2%84%A4) (char %E2%84%9A) (char %E2%84%9D) (char %E2%84%82) (char %E2%88%87) (char %3F) (char %21)))) (concept grammar.identifier))
(rule escaped_identifier token (seq (literal %C2%AB) (repeat0 (class negated (char %C2%BB))) (literal %C2%BB)) (concept grammar.escaped-identifier))
(rule float token (lexicalPrecedence 1 (seq (repeat1 (class plain (range 0 9))) (literal .) (optional (repeat1 (class plain (range 0 9)))))) (concept grammar.float))
(rule number normal (choice unordered (alias unnamed_token (token (repeat1 (class plain (range 0 9))))) (alias unnamed_token (token (seq (literal 0x) (repeat1 (class plain (range 0 9) (range a f) (range A F)))))) (alias unnamed_token (token (seq (literal 0b) (repeat1 (class plain (char 0) (char 1)))))) (alias unnamed_token (token (seq (literal 0o) (repeat1 (class plain (range 0 7))))))) (concept grammar.number))
(rule string normal (seq (literal %22) (repeat0 (choice unordered (ref string_content) (ref escape_sequence) (ref interpolation))) (literal %22)) (concept grammar.string))
(rule interpolated_string normal (seq (capture labeled prefix (choice unordered (token (seq (literal s%21) (not (ref word_characters)))) (token (seq (literal r%21) (not (ref word_characters)))) (token (seq (literal m%21) (not (ref word_characters)))))) (ref string)) (concept grammar.template-string))
(rule string_content silent (alias unnamed_token (immediateToken (lexicalPrecedence 1 (repeat1 (class negated (char %22) (char %5C) (char %7B)))))) (concept grammar.string-content) (source-names (tree-sitter _string_content)))
(rule escape_sequence silent (alias escape_sequence (immediateToken (seq (literal %5C) (choice unordered (class plain (char %5C) (char %27) (char %22) (char n) (char r) (char t) (char 0)) (seq (literal x) (repeat 2 2 (class plain (range 0 9) (range a f) (range A F)))) (seq (literal u) (repeat 4 4 (class plain (range 0 9) (range a f) (range A F)))) (seq (literal u%7B) (repeat1 (class plain (range 0 9) (range a f) (range A F))) (literal %7D)) (seq (literal %0A) (repeat0 (class plain (char %20) (char %09) (char %0A) (char %0D) (char %0C) (char %0B)))))))) (concept grammar.escape-sequence))
(rule interpolation normal (seq (literal %7B) (ref expression) (literal %7D)) (concept grammar.template-substitution))
(rule character normal (seq (literal %27) (choice unordered (alias unnamed_token (token (class negated (char %27) (char %5C)))) (alias unnamed_token (token (seq (literal %5C) (class negated (char %0A)))))) (literal %27)) (concept grammar.character-literal) (source-names (tree-sitter char)))
(rule hole token (seq (literal _) (not (ref word_characters))) (concept grammar.hole))
(rule centered_dot normal (literal %C2%B7) (concept grammar.centered-dot) (source-names (tree-sitter cdot)))
(rule synthetic_hole token (seq (literal %3F) (class plain (char _) (range a z) (range A Z)) (repeat0 (class plain (range a z) (range A Z) (range 0 9) (char _)))) (concept grammar.synthetic-hole))
(rule quoted_name normal (seq (literal %60) (ref identifier)) (concept grammar.quoted-name))
(rule double_quoted_name normal (seq (literal %60%60) (ref identifier)) (concept grammar.double-quoted-name))
(rule syntax_quotation normal (seq (literal %60) (immediateToken (literal %28)) (optional (alias unnamed_token (immediateToken (ref syntax_quotation_body)))) (literal %29)) (concept grammar.syntax-quotation))
(rule ellipsis token (literal ..) (concept grammar.ellipsis))
(rule sorry token (seq (literal sorry) (not (ref word_characters))) (concept grammar.sorry-placeholder))
(rule boolean silent (choice unordered (ref true) (ref false)) (concept grammar.boolean-value) (source-names (tree-sitter _boolean)))
(rule true normal (choice unordered (token (seq (literal true) (not (ref word_characters)))) (token (seq (literal True) (not (ref word_characters))))) (concept grammar.true-constant))
(rule false normal (choice unordered (token (seq (literal false) (not (ref word_characters)))) (token (seq (literal False) (not (ref word_characters))))) (concept grammar.false-constant))
(rule comment token (choice unordered (seq (literal --) (repeat0 (class negated (char %0A)))) (seq (literal %2F-) (seq (repeat0 (class negated (char -))) (repeat0 (seq (repeat1 (literal -)) (class negated (char -) (char %2F)) (repeat0 (class negated (char -))))) (repeat0 (literal -))) (literal -%2F))) (concept grammar.comment))
(rule word_characters token (seq (class plain (char _) (range a z) (range A Z) (range %CE%B1 %CF%89) (range %CE%91 %CE%A9) (char %E2%84%95) (char %E2%84%A4) (char %E2%84%9A) (char %E2%84%9D) (char %E2%84%82) (char %E2%88%87)) (repeat0 (class plain (char _) (range a z) (range A Z) (range 0 9) (char %27) (range %CE%B1 %CF%89) (range %CE%91 %CE%A9) (char %E2%84%95) (char %E2%84%A4) (char %E2%84%9A) (char %E2%84%9D) (char %E2%84%82) (char %E2%88%87) (char %3F) (char %21)))) (concept grammar.word-characters))