\begin{syntax} theory ::= "theory" uident-nq label* decl* "end" \ decl ::= "type" type-decl ("with" type-decl)* ; | "constant" constant-decl ; | "function" function-decl ("with" logic-decl)* ; | "predicate" predicate-decl ("with" logic-decl)* ; | "inductive" inductive-decl ("with" inductive-decl)* ; | "coinductive" inductive-decl ("with" inductive-decl)* ; | "axiom" ident-nq ":" formula ; | "lemma" ident-nq ":" formula ; | "goal" ident-nq ":" formula ; | "use" imp-exp tqualid ("as" uident)? ; | "clone" imp-exp tqualid ("as" uident)? subst? ; | "namespace" "import"? uident-nq decl* "end" ; \ logic-decl ::= function-decl ; | predicate-decl \ constant-decl ::= lident-nq label* ":" type ; | lident-nq label* ":" type "=" term \ function-decl ::= lident-nq label* type-param* ":" type ; | lident-nq label* type-param* ":" type "=" term \ predicate-decl ::= lident-nq label* type-param* ; | lident-nq label* type-param* "=" formula \ inductive-decl ::= lident-nq label* type-param* "=" ; "|"? ind-case ("|" ind-case)* ; \ ind-case ::= ident-nq label* ":" formula ; \ imp-exp ::= ("import" | "export")? \ subst ::= "with" ("," subst-elt)+ \ subst-elt ::= "type" lqualid "=" lqualid ; | "function" lqualid "=" lqualid ; | "predicate" lqualid "=" lqualid ; | "namespace" (uqualid | ".") "=" (uqualid | ".") ; | "lemma" qualid ; | "goal" qualid ; \ tqualid ::= uident | ident ("." ident)* "." uident ; \ type-decl ::= lident-nq label* ("'" lident-nq label*)* type-defn; % \end{syntax}