; DO NOT EDIT THIS FILE MANUALLY
; It is generated automatically with 'make bnf'.

QID ::= [UID "."]+ UID

<switch> ::= "on"
           | "off"

<side> ::= "left"
         | "right"

<assert> ::= "assert"
           | "assertnot"

<term_alone> ::= <term> EOF

<qid_alone> ::= <qid> EOF

<search_query_alone> ::= <search_query> EOF

<command> ::= "opaque" <qid_or_int> ";"
            | "require" "open" <path>* ";"
            | "require" <path>* ";"
            | "require" <path> "as" <uid> ";"
            | "open" <path>* ";"
            | <modifier>* "symbol" <uid_or_int> <param_list>* ":" <term>
              [<proof>] ";"
            | <modifier>* "symbol" <uid_or_int> <param_list>* [":" <term>]
              "≔" <term_proof> ";"
            | [<exposition>] <param_list>* "inductive" <inductive> ("with"
              <inductive>)* ";"
            | "rule" <rule> ("with" <rule>)* ";"
            | "builtin" <stringlit> "≔" <qid_or_int> ";"
            | "coerce_rule" <rule> ";"
            | "unif_rule" <unif_rule> ";"
            | "notation" <qid_or_int> <notation> ";"
            | <query> ";"
            

<query> ::= <assert> <param_list>* "⊢" <term> ":" <term>
          | <assert> <param_list>* "⊢" <term> "≡" <term>
          | "compute" <term>
          | "print" [<qid_or_rule>]
          | "proofterm"
          | "debug" ("+"|"-") <string>
          | "flag" <stringlit> <switch>
          | "prover" <stringlit>
          | "prover_timeout" <nat>
          | "verbose" <nat>
          | "type" <term>
          | "search" <stringlit>

<qid_or_rule> ::= <qid>
                | "unif_rule"
                | "coerce_rule"

<path> ::= UID
         | QID

<modifier> ::= [<side>] "associative"
             | "commutative"
             | "constant"
             | "injective"
             | "opaque"
             | "sequential"
             | <exposition>

<exposition> ::= "private"
               | "protected"

<uid> ::= UID

<uid_or_int> ::= <uid>
               | <int>

<qid_or_int> ::= <qid>
               | <int>

<param_list> ::= <param>
               | "(" <param>+ ":" <term> ")"
               | "[" <param>+ [":" <term>] "]"

<param> ::= <uid>
          | <nat>
          | "_"

<term> ::= <bterm>
         | <saterm>
         | <saterm> <bterm>
         | <saterm> "→" <term>

<bterm> ::= "`" <term_id> <binder>
          | "Π" <binder>
          | "λ" <binder>
          | "let" <uid> <param_list>* [":" <term>] "≔" <term> "in" <term>

<saterm> ::= <aterm>+

<aterm> ::= <term_id>
          | "_"
          | "TYPE"
          | "?" UID [<env>]
          | "$" UID [<env>]
          | "(" <term> ")"
          | "[" <term> "]"
          | <nat>
          | "-"<nat>

<env> ::= "." "[" [<term> (";" <term>)*] "]"

<term_id> ::= <qid>
            | <qid_expl>

<qid> ::= UID
        | QID

<qid_expl> ::= "@" UID
             | "@" QID

<binder> ::= <param_list>+ "," <term>
           | <param> ":" <term> "," <term>

<term_proof> ::= <term>
               | <proof>
               | <term> <proof>

<proof> ::= "begin" <subproof>+ <proof_end>
          | "begin" [<proof_steps>] <proof_end>

<subproof> ::= "{" [<proof_steps>] "}"

<proof_steps> ::= <proof_step>
                | <proof_step> ";"
                | <proof_step> ";" <proof_steps>

<proof_step> ::= <tactic> <subproof>*

<proof_end> ::= "abort"
              | "admitted"
              | "end"

<tactic> ::= <query>
           | "admit"
           | "apply" <term>
           | "assume" <param>+
           | "fail"
           | "generalize" <uid>
           | "have" <uid> ":" <term>
           | "induction"
           | "refine" <term>
           | "reflexivity"
           | "remove" <uid>+
           | "rewrite" [<side>] [<rw_patt_spec>] <term>
           | "simplify" [<qid_or_int>]
           | "solve"
           | "symmetry"
           | "try" <tactic>
           | "why3" [<stringlit>]

<rw_patt> ::= <term>
            | "in" <term>
            | "in" <uid> "in" <term>
            | <term> "in" <term> ["in" <term>]
            | <term> "as" <uid> "in" <term>

<rw_patt_spec> ::= "." "[" <rw_patt> "]"

<inductive> ::= <uid> <param_list>* ":" <term> "≔" ["|"] [<constructor>
                ("|" <constructor>)*]

<constructor> ::= <uid_or_int> <param_list>* ":" <term>

<rule> ::= <term> "↪" <term>

<unif_rule> ::= <equation> "↪" "[" <equation> (";"
                <equation>)* "]"

<equation> ::= <term> "≡" <term>

<notation> ::= "infix" [<side>] <float_or_int>
             | "postfix" <float_or_int>
             | "prefix" <float_or_int>
             | "quantifier"

<float_or_int> ::= <float>
                 | <int>

<int> ::= "-"<nat>
        | <nat>

<maybe_generalize> ::= ["generalize"]

<where> ::= UID <maybe_generalize>

<asearch_query> ::= "type" <where> <aterm>
                  | "rule" <where> <aterm>
                  | UID <where> <aterm>
                  | "(" <search_query> ")"

<csearch_query> ::= <asearch_query> ("," <asearch_query>)*

<ssearch_query> ::= <csearch_query> (";" <csearch_query>)*

<search_query> ::= <ssearch_query>
                 | <search_query> "|" <qid>