1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
% test16.4.ott auxfn and subst test
% multiple types, multiple mutually dependent auxfn but with disjoint domains
% ISA FAILS, but succeeds if we hand-edit the consts and primrecs into single ones
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 g(b2) +)
| C :: :: C (+ f={} +)
b :: 'b_' ::=
| x :: :: x (+ g=x +)
| B a1 b2 :: :: A (+ g=f(a1) union g(b2) +)
| C :: :: C (+ g={} +)
substitutions
single a value_name :: subst
multiple a value_name :: msubst
|
