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
|
% test16.1.ott auxfn and subst test
% multiple type, single auxfn
% ISA FAILS but in a fixable way - if we collect together the consts
%
% aux_f_a :: "a => value_name list"
% aux_f_b :: "b => value_name list"
%
% properly, and the corresponding primrecs into a single primrec, it succeeds.
metavar value_name , x ::=
{{ isa string }} {{ coq nat }} {{ coq-equality }} {{ hol string }}
grammar
a :: 'a_' ::=
| x :: :: x (+ f=x +)
| A a1 b2 :: :: A (+ f=f(a1) union f(b2) +)
| C :: :: C (+ f={} +)
b :: 'b_' ::=
| x :: :: x (+ f=x +)
| B a1 b2 :: :: A (+ f=f(a1) union f(b2) +)
| D :: :: C (+ f={} +)
substitutions
single a value_name :: subst
multiple a value_name :: msubst
|
