theory.bnf 1.64 KB
Newer Older
1
\begin{syntax}
2
  theory ::= "theory" uident-nq label* decl* "end"
3
  \
4
  decl ::= "type" type-decl ("with" type-decl)* ;
5
    | "constant" constant-decl ;
6 7
    | "function" function-decl ("with" logic-decl)* ;
    | "predicate" predicate-decl ("with" logic-decl)* ;
8
    | "inductive" inductive-decl ("with" inductive-decl)* ;
9
    | "coinductive" inductive-decl ("with" inductive-decl)* ;
10 11 12
    | "axiom" ident-nq ":" formula 	   ;
    | "lemma" ident-nq ":" formula 	   ;
    | "goal"  ident-nq ":" formula 	   ;
13 14
    | "use" imp-exp tqualid ("as" uident)?     ;
    | "clone" imp-exp tqualid ("as" uident)? subst? ;
15
    | "namespace" "import"? uident-nq decl* "end" ;
16
  \
17 18 19
  logic-decl ::= function-decl ;
    | predicate-decl
  \
20 21
  constant-decl ::= lident-nq label* ":" type ;
    | lident-nq label* ":" type "=" term
22
  \
23 24
  function-decl ::= lident-nq label* type-param* ":" type ;
    | lident-nq label* type-param* ":" type "=" term
25
  \
26 27
  predicate-decl ::= lident-nq label* type-param* ;
    | lident-nq label* type-param* "=" formula
28
  \
29
  inductive-decl ::= lident-nq label* type-param* "=" ;
30 31
                     "|"? ind-case ("|" ind-case)* ;
  \
32
  ind-case ::= ident-nq label* ":" formula ;
33
  \
34 35 36 37 38
  imp-exp ::= ("import" | "export")?
  \
  subst ::= "with" ("," subst-elt)+
  \
  subst-elt ::= "type" lqualid "=" lqualid ;
39 40
    | "function" lqualid "=" lqualid          ;
    | "predicate" lqualid "=" lqualid         ;
41
    | "namespace" (uqualid | ".") "=" (uqualid | ".")  ;
42 43
    | "lemma" qualid 	  		   ;
    | "goal"  qualid			   ;
44
  \
45
  tqualid ::= uident | ident ("." ident)* "." uident ;
46 47
  \
  type-decl ::= lident-nq label* ("'" lident-nq label*)* type-defn; %
48
\end{syntax}