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
|
% test15.4.ott is_v test
% mtutual recursion between a single upper/lower type pair, with dot forms
indexvar index , n ::= {{ isa nat }} {{ coq nat }} {{ coq-equality }}
{{ hol num }} {{ ocaml int }}
metavar x ::= {{ isa nat }} {{ coq nat }} {{ coq-equality }} {{ hol string }} {{ ocaml int }}
grammar
a :: 'a_' ::=
| x :: :: Ax
| AA :: :: AA
| A a :: :: a
| C a1 .. an :: :: C
| D av1 .. avn :: :: D
| CC a1 .. an :: :: CC
| DD av1 .. avn :: :: DD
av :: 'av_' ::=
| A a :: :: a
| C a1 .. an :: :: C
| D av1 .. avn :: :: D
subrules
av <:: a
freevars
a x :: fv
|
