blob: 156f0286ea889c9296d60be1759c48ab31c034f0 (
plain)
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
|
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 : var Syntax.TZ,
Tbase Syntax.TZ x19 = x + x9;
Tbase Syntax.TZ x20 = x0 + x10;
Tbase Syntax.TZ x21 = x1 + x11;
Tbase Syntax.TZ x22 = x2 + x12;
Tbase Syntax.TZ x23 = x3 + x13;
Tbase Syntax.TZ x24 = x4 + x14;
Tbase Syntax.TZ x25 = x5 + x15;
Tbase Syntax.TZ x26 = x6 + x16;
Tbase Syntax.TZ x27 = x7 + x17;
Tbase Syntax.TZ x28 = x8 + x18;
(Return x19, Return x20, Return x21, Return x22, Return x23,
Return x24, Return x25, Return x26, Return x27, Return x28)
: 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 ->
Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
Tbase Syntax.TZ)
Argument scope is [function_scope]
|
