blob: 4e361cd8d1732753355924fe196310141381d5a1 (
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
|
raddW =
fun var : Syntax.base_type -> Type =>
λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : var Syntax.TZ,
Tbase Syntax.TZ x15 = x + x7;
Tbase Syntax.TZ x16 = x0 + x8;
Tbase Syntax.TZ x17 = x1 + x9;
Tbase Syntax.TZ x18 = x2 + x10;
Tbase Syntax.TZ x19 = x3 + x11;
Tbase Syntax.TZ x20 = x4 + x12;
Tbase Syntax.TZ x21 = x5 + x13;
Tbase Syntax.TZ x22 = x6 + x14;
(Return x15, Return x16, Return x17, Return x18, Return x19,
Return x20, Return x21, Return x22)
: 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 ->
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]
|
