File tree Expand file tree Collapse file tree 3 files changed +40
-0
lines changed Expand file tree Collapse file tree 3 files changed +40
-0
lines changed Original file line number Diff line number Diff line change @@ -17,3 +17,5 @@ fun D D' : D.type =>
1717 |}
1818|}
1919 : D.type -> D.type -> D.type
20+
21+ Arguments Datatypes_prod__canonical__compress_coe_D D D'
Original file line number Diff line number Diff line change 1+ Datatypes_prod__canonical__compress_coe_D =
2+ fun D D' : D.type =>
3+ {|
4+ D.sort := D.sort D * D.sort D';
5+ D.class :=
6+ {|
7+ D.compress_coe_hasA_mixin :=
8+ prodA (compress_coe_D__to__compress_coe_A D)
9+ (compress_coe_D__to__compress_coe_A D');
10+ D.compress_coe_hasB_mixin :=
11+ prodB tt (compress_coe_D__to__compress_coe_B D)
12+ (compress_coe_D__to__compress_coe_B D');
13+ D.compress_coe_hasC_mixin :=
14+ prodC tt tt (compress_coe_D__to__compress_coe_C D)
15+ (compress_coe_D__to__compress_coe_C D');
16+ D.compress_coe_hasD_mixin := prodD D D'
17+ |}
18+ |}
19+ : D.type -> D.type -> D.type
Original file line number Diff line number Diff line change 1+ Datatypes_prod__canonical__compress_coe_D =
2+ fun D D' : D.type =>
3+ {|
4+ D.sort := D.sort D * D.sort D';
5+ D.class :=
6+ {|
7+ D.compress_coe_hasA_mixin :=
8+ prodA (compress_coe_D__to__compress_coe_A D)
9+ (compress_coe_D__to__compress_coe_A D');
10+ D.compress_coe_hasB_mixin :=
11+ prodB tt (compress_coe_D__to__compress_coe_B D)
12+ (compress_coe_D__to__compress_coe_B D');
13+ D.compress_coe_hasC_mixin :=
14+ prodC tt tt (compress_coe_D__to__compress_coe_C D)
15+ (compress_coe_D__to__compress_coe_C D');
16+ D.compress_coe_hasD_mixin := prodD D D'
17+ |}
18+ |}
19+ : D.type -> D.type -> D.type
You can’t perform that action at this time.
0 commit comments