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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
raddW =
fun var : Syntax.base_type -> Type =>
λ
x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20
x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37
x38 : var Syntax.TZ,
Tbase Syntax.TZ x39 = x + x19;
Tbase Syntax.TZ x40 = x0 + x20;
Tbase Syntax.TZ x41 = x1 + x21;
Tbase Syntax.TZ x42 = x2 + x22;
Tbase Syntax.TZ x43 = x3 + x23;
Tbase Syntax.TZ x44 = x4 + x24;
Tbase Syntax.TZ x45 = x5 + x25;
Tbase Syntax.TZ x46 = x6 + x26;
Tbase Syntax.TZ x47 = x7 + x27;
Tbase Syntax.TZ x48 = x8 + x28;
Tbase Syntax.TZ x49 = x9 + x29;
Tbase Syntax.TZ x50 = x10 + x30;
Tbase Syntax.TZ x51 = x11 + x31;
Tbase Syntax.TZ x52 = x12 + x32;
Tbase Syntax.TZ x53 = x13 + x33;
Tbase Syntax.TZ x54 = x14 + x34;
Tbase Syntax.TZ x55 = x15 + x35;
Tbase Syntax.TZ x56 = x16 + x36;
Tbase Syntax.TZ x57 = x17 + x37;
Tbase Syntax.TZ x58 = x18 + x38;
(Return x39, Return x40, Return x41, Return x42, Return x43,
Return x44, Return x45, Return x46, Return x47, Return x48,
Return x49, Return x50, Return x51, Return x52, Return x53,
Return x54, Return x55, Return x56, Return x57, Return x58)
: forall var : Syntax.base_type -> Type,
expr Syntax.base_type Syntax.op
(Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
... * ... * Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ)
Argument scope is [function_scope]
|
