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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
metavar terminal, t ::= {{ isa string }} {{ coq nat }} {{ hol string }}
metavar metavarroot, mvr ::= {{ isa string }} {{ coq nat }} {{ hol string }}
metavar nontermroot, ntr ::= {{ isa string }} {{ coq nat }} {{ hol string }}
metavar suffix, suff ::= {{ isa string }} {{ coq nat }} {{ hol string }}
metavar auxfn, f ::= {{ isa string }} {{ coq nat }} {{ hol string }}
metavar prodname, pn ::= {{ isa string }} {{ coq nat }} {{ hol string }}
indexvar index, i, j, n, m ::= {{ isa string }} {{ coq nat }} {{ hol string }}
grammar
'metavar' :: 'mv_' ::=
| metavarroot suffix :: :: 1
nonterm :: 'nt_' ::=
| nontermroot suffix :: :: 1
element :: 'e_' ::=
| terminal :: :: tm
| 'metavar' :: :: mv
| nonterm :: :: nt
mse :: 'mse_' ::=
| 'metavar' :: :: mv
| nonterm :: :: nt
| auxfn ( nonterm ) :: :: f
| mse union mse' :: :: union
| {} :: :: empty
bindspec, bs :: 'bs_' ::=
| 'bind' mse in nonterm :: :: bind
| auxfn = mse :: :: auxfn
prod {{ hol production }} :: 'p_' ::=
| '|' element1 .. elementm '::' '::' prodname '(+' bindspec1 .. bindspecn '+)' :: :: 1
rule :: 'r_' ::=
| nontermroot '::' '''' '::=' prod1 .. prodm :: :: 1
grammar_rules :: 'g_' ::=
| 'grammar' rule1 .. rulem :: :: 1
formula :: 'formula_' ::=
| judgement :: :: judgement
terminals :: '' ::=
| '{}' :: :: quote {{ tex \texttt{\{\} } }}
| '(' :: :: lparen {{ tex \texttt{(} }}
| ')' :: :: rparen {{ tex \texttt{)} }}
| '(+' :: :: lparenplus {{ tex \texttt{(+} }}
| '+)' :: :: rparenplus {{ tex \texttt{+)} }}
| '''' :: :: quotequote {{ tex \texttt{''} }}
| '::' :: :: coloncolon {{ tex \texttt{::} }}
| '::=' :: :: coloncoloneq {{ tex \texttt{::=} }}
| 'grammar' :: :: tgrammar {{ tex \texttt{grammar} }}
| 'bind' :: :: bind {{ tex \texttt{bind} }}
| 'in' :: :: in {{ tex \texttt{in} }}
| 'union' :: :: union {{ tex \texttt{union} }}
|
