::= [ "."]+ ::= | ::= "opaque" ";" | "require" + ";" | "require" [["private"] "open"] + ";" | "require" "as" ";" | ["private"] "open" + ";" | [] * "symbol" * ":" [ | "≔" ] ";" | [] * "symbol" * "≔" [] ";" | [] * "inductive" ("with" )* ";" | "rule" ("with" )* ";" | "builtin" "≔" ";" | "coerce_rule" ";" | "unif_rule" ";" | "notation" ";" | ";" ::= "private" | "protected" ::= "left" | "right" ::= [] "associative" | "commutative" | "constant" | "injective" | "opaque" | "sequential" ::= * ":" "≔" ["|"] [ ("|" )*] ::= * ":" ::= "↪" ::= "↪" "[" (";" )* "]" ::= "≡" ::= "infix" [] | "postfix" | "prefix" | "quantifier" ::= | ::= | "(" + ":" ")" | "[" + [":" ] "]" ::= | "_" ::= ["→" ] | [] ::= * ::= | "let" * [":" ] "≔" "in" ::= "λ" | "Π" | "`" ["@"] ::= ["@"] | "_" | "TYPE" | "?" [] | "$" [] | "(" ")" | | ::= | "[" "]" ::= "." "[" [ (";" )*] "]" ::= + "," | ":" "," ::= | | ::= "begin" + | "begin" [] ::= "{" [] "}" ::= [";"] | ";" ::= * ::= "end" | "abort" | "admitted" ::= | "admit" | "apply" | "assume" + | "change" | "eval" | "fail" | "generalize" | "have" ":" | "induction" | "orelse" | "refine" | "reflexivity" | "remove" + | "repeat" | "rewrite" [] ["." "[" "]"] | "set" "≔" | "simplify" | "simplify" | "simplify" "rule" "off" | "solve" | "symmetry" | "try" | "why3" [] ::= | "in" | "in" "in" | "in" ["in" ] | "as" "in" ::= "assert" | "assertnot" ::= ":" | "≡" ::= "on" | "off" ::= * "⊢" | "compute" | "print" [ | "unif_rule" | "coerce_rule"] | "proofterm" | "debug" | "debug" ("+"|"-") + | "flag" | "flag" | "prover" | "prover_timeout" | "verbose" | "type" | "search" ::= "=" | ">" | ">=" | "≥" ::= "concl" | "hyp" | "spine" | "rule" | "lhs" | "rhs" ::= "name" "=" | ("type"|"anywhere") ("≥"|">=") ["generalize"] | ["generalize"] | "(" ")" ::= ("," )* ::= (";" )* ::= | "|"