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
|
% test17.14.ott dot form test
metavar value_name , x ::=
{{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }}
indexvar index , n ::= {{ isa nat }} {{ coq nat }} {{ coq-equality }} {{ hol num }}
grammar
a :: 'a_' ::=
| x :: :: x
| E ( ( c1 , c'1 , c''1 ) .. ( cn , c'n , c''n ) ) :: :: E
av :: 'av_' ::=
| E ( ( c1 , c'1 , c''1 ) .. ( cn , c'n , c''n ) ) :: :: E
c :: 'c_' ::=
| C a1 .. an :: :: C
subrules
av <:: a
substitutions
single a value_name :: subst
freevars
a value_name :: fv
|
