blob: c1012d128e317c7ed21f7f8893b87534bcc0333f (
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
|
raddW =
fun var : Syntax.base_type -> Type =>
λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 : var Syntax.TZ,
Tbase Syntax.TZ x9 = x + x4;
Tbase Syntax.TZ x10 = x0 + x5;
Tbase Syntax.TZ x11 = x1 + x6;
Tbase Syntax.TZ x12 = x2 + x7;
Tbase Syntax.TZ x13 = x3 + x8;
(Return x9, Return x10, Return x11, Return x12, Return x13)
: 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 ->
Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
Tbase Syntax.TZ * Tbase Syntax.TZ)
Argument scope is [function_scope]
|
