1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
embed
{{ coq
(* coq preamble embed *) }}
{{ isa
(* isa preamble embed *) }}
metavar ident , x ::= {{ isa string }} {{ coq nat }} {{ lex [A-Z]+ }}
embed {{ coq (* after metavar embed *) }}
grammar
T :: T_ ::=
| int :: :: integer
| float :: :: float
E :: E_ ::= {{ isa (ident*type) list }} {{ coq list (ident * T) }}
| empty :: :: empty {{ coq nil }}
{{ isa [] }}
| E , x : T :: :: ident {{ coq cons ([[x]],[[T]]) [[E]] }}
{{ isa [[x]] :: [[T]] }}
F :: F_ ::= {{ coq list (ident * ident) }}
{{ isa (ident*ident) list }}
| empty :: :: empty {{ coq nil }}
{{ isa [] }}
| E , x1 : x2 :: :: ident {{ coq (cons ([[x1]],[[x2]]) [[E]]) }}
{{ isa ([[x1]],[[x2]])#[[E]] }}
embed {{ coq (* after rules embed *) }}
|
